perm filename THE[P,JRA] blob
sn#193494 filedate 1975-12-23 generic text, type T, neo UTF8
.font 1 "25fr1" << text >>
.font 2 "25fri1" << italics >>
.font 3 "25fg" << ECL code >>
.font 4 "gls;foo" << weird characters >>
.font 5 "25vqxb" << quuxy boldface >>
.font 6 "36vbee" << headings >>
.font 7 "snoopy" << random snoopy picture >>
.select 1
.textfont ← 1
.eclfont ← 3
.chapterheadfont ← 6
.sectionheadfont ← 5
.subsecheadfont ← 5
.subsubsecheadfont ← 5
.smallheadfont ← 1
.if xcribl then hauwide ← 80 else hauwide ← 70
.page frame 59 high (hauwide) wide
.macro typvar(name) ⊂ tty←"name="&name ⊃
.margins 1050,1170;
.typvar page!height; typvar page!width;
.text area text lines 5 to (page!height-3)
.title area heading line 1
.title area footing line page!height
.place text
.turn on "%#{αβ↓_→∂[]"
.turn on "↑" for "\" << need backslash for ECL code >>
.turn on "`" for "↑" << need something for superscripts >>
.turn off "-"
.tabbreak
.at null ⊂ if not filling then skip 1 ⊃
.double space
.indent 8,0,0
.<< ⊗⊗foo⊗ makes foo into a footnote >>
.count ftnote inline printing "1"
.at "⊗⊗" cruft "⊗" ⊂
. next ftnote; "`[%2"; ftnote! ; "%*]";
. send foot ⊂
. begin "footnote {ftnote!}"
. select textfont
. fill
. preface 1
. single space
. indent 0,0
{ftnote!}. cruft
. break
. end "footnote {ftnote!}" ⊃ ⊃
.footsep ← "←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←←"
.<< feature for section titles and numbers in footing >>
.sectiontitle ← "lose lose" << for safety's sake >>
.sectionnumber ← "lose lose"
.nextsectiontitle ← "losey losey"
.nextsectionnumber ← "losey losey"
.sectionlevel ← 99
.before page ⊂⊃
.after page ⊂
. begin "titlesblock"
. at "/" wds "/" ⊂
. if xcribl then start "/" }%3{}wds%*{ end "/"
. else start "/" }wds{ end "/" ⊃
. standard titles
. end "titlesblock"
. sectionlevel ← 99
. sectiontitle ← nextsectiontitle
. sectionnumber ← nextsectionnumber ⊃
.macro sectitle(level,name,εnumber,title) ⊂
. nextsectiontitle ← "title"
. nextsectionnumber ← "name number"
. if level < sectionlevel then
. start
. sectionlevel ← level
. sectiontitle ← nextsectiontitle
. sectionnumber ← nextsectionnumber
. end ⊃
.count chaptercount
.macro chapter(tag, title) ⊂
. next page
. group skip 7
. begin "chapter!block"
. nofill indent 0 center
. select chapterheadfont
. tag: next chaptercount!
. chaptertitle ← "Chapter " & chaptercount! & ". title"
Chapter {chaptercount!}
.skip 1
title
. skip 3
. sectitle(1,Chapter,chaptercount!,|title|)
. end "chapter!block"
. send contents ⊂
.begin "tag contents"
.skip 1
%5Chapter {chaptercount!}.↑title→{page!}
.end "tag contents" ⊃
. ⊃
.count sectioncount in chaptercount printing "!.1"
.macro section(tag, title) ⊂
. if lines < (5 * spread) then next page
. tag: next sectioncount!
. skip (spread+2)
. once nofill indent 0
. select sectionheadfont
{sectioncount!}. title
. skip 1
. sectitle(2,Section,sectioncount!,|title|)
.send contents ⊂
.begin "tag contents"
.break
%5↑{sectioncount!}.↑title→{page!}
.end "tag contents"⊃
. ⊃
.count subseccount in sectioncount printing "!.1"
.macro subsec(tag, title) ⊂
. if lines < (5 * spread) then next page
. tag: next subseccount!
. skip (spread+2)
. once nofill indent 0
. select subsecheadfont
{subseccount!}. title
. skip 1
. sectitle(3,Section,subseccount!,|title|)
.send contents ⊂
.begin "tag contents"
.break
%5↑↑{subseccount!}.↑title→{page!}
.end "tag contents" ⊃
. ⊃
.count subsubseccount in subseccount printing "!.1"
.macro subsubsec(tag, title) ⊂
. if lines < (5 * spread) then next page
. tag: next subsubseccount!
. skip (spread+2)
. once nofill indent 0
. select subsubsecheadfont
{subsubseccount!}. title
. skip 1
. sectitle(4,Section,subsubseccount!,|title|)
.send contents ⊂
.begin "tag contents"
.break
%5↑↑↑{subsubseccount!}.↑title→{page!}
.end "tag contents" ⊃
. ⊃
.macro smallhead(title) ⊂
. if lines < (5 * spread) then next page
. skip (spread+1)
. once nofill indent 0
. select smallheadfont
↓_title_↓
. skip 1 ⊃
.macro beginecl ⊂
. begin "ecl!block"
. group
. nofill
. indent 0,0
. narrow 4,0
. tabs 5,9,13,17,21,25,29,33,37,41
. select eclfont
. skip spread
. ⊃
.macro endecl ⊂
. skip 1
. end "ecl!block"
. continue ⊃
. << $foo$ puts foo in italics >>
.at "$" wds "$" ⊂
. if xcribl then start "$" }%2{}wds%*{ end "$"
. else start "$" }↓_wds_↓{ end "$" ⊃
. << /foo/ puts foo in the ecl font >>
.at "/" wds "/" ⊂
. if xcribl then start "/" }%3{}↓_wds_↓%*{ end "/"
. else start "/" }↓_wds_↓{ end "/" ⊃
. << εfooε puts foo in the super-bold font >>
.at "ε" ch "ε" ⊂
. if xcribl then start "ε" }%5αch%*{ end "ε"
. else start "ε" }αch∂-1αch∂-1αch∂-1αch∂-1αch∂-1αch∂-1αch{ end "ε" ⊃
.at "@" tag "@" ⊂
. [4] tag ⊃
.at "∞" ⊂ }%5α|%*↑{ ⊃ << boldface | plus tab >>
.<< by convention, ∀x puts the character x in the weird font >>
.at "∀←" ⊂
. if xcribl then start "∀←" }%4α←%*{ end "∀←"
. else start "∀←" }<-{ end "∀←" ⊃
.at "∀→" ⊂
. if xcribl then start "∀→" }%4α→%*{ end "∀→"
. else start "∀→" }=>{ end "∀→" ⊃
.at "∀↔" ⊂
. if xcribl then start "∀↔" }%4α↔%*{ end "∀↔"
. else start "∀↔" }<=>{ end "∀↔" ⊃
.at "∀~" ⊂
. if xcribl then start "∀~" }%4α~%*{ end "∀~"
. else start "∀~" }=∂-1/{ end "∀~" ⊃
.at "∀mu" ⊂
. if xcribl then start "∀mu" }%4α∨%*{ end "∀mu"
. else start "∀mu" }↓_mu_↓{ end "∀mu" ⊃
.<< bibliography entries here, sent to end of manuscript >>
.<< this is so will not needforward references to tags, >>
.<< which could screw up the justification >>
.macro ref(tag, refname, body) ⊂
. tag ← "refname"
.send bibliography ⊂
. begin "ref refname" group
[refname]
.continue
body
. skip end "ref refname" ⊃ ⊃
.ref courtois,Courtois#71,|Courtois, P.J., Heymans, F., Parnas, D.L. Concurrent Control with "Readers" and "Writers". $Comm. ACM 14$, 10 (October 1971), 667-668.|
.ref genuys,Dijkstra#65,|Dijkstra, E.W. Cooperating Sequential Processes. Technological University, Eindhoven, 1965. Reprinted in $Programming Languages$, F. Genuys (Ed.), Academic Press, New York, 1968.|
.ref THEsystem,Dijkstra#68,|Dijkstra, E.W. The Structure of "THE"-multiprogramming System. $Comm. ACM 11$, 5 (May 1968), 341-346.|
.ref eclmanual,ECL#Manual#74,|$ECL Programmer's Manual.$ Report α#23-74. Center for Research in Computing Technology, Harvard University, Cambridge, Mass., December 1974.|
.ref hoare,Hoare#74,|Hoare, C.A.R. Monitors: An Operating System Structuring Concept. $Comm. ACM 17$, 10 (October 1974), 549-557.|
.ref synver,Griffiths#74,|Griffiths, Patricia. SYNVER: A System for the Automatic Synthesis and Verification of Synchronization Processes. $Proceedings of the ACM$ (November 1974) 167-173.|
.ref salpaper,Griffiths#75a,|Griffiths, Patricia. SAL: A Very High Level Specification Language. Center for Research in Computing Technology, Harvard University, Cambridge, Mass., February 1975.|
.ref patsthesis,Griffiths#75b,|Griffiths, Patricia. SYNVER: A System for the Automatic Synthesis and Verification of Synchronization Processes. Ph.D. thesis. Harvard University, Cambridge, Mass., 1975.|
.ref macsymamanual,MACSYMA#74,|$MACSYMA Reference Manual.$ Mathlab Group, Project MAC, M.I.T., Cambridge, Mass., September 1974.|
.ref moon,Moon#74,|Moon, David A. $MacLISP Reference Manual.$ Project MAC, M.I.T., Cambridge, Mass., April 1974.|
.ref chuck,Prenner#72,|Prenner, Charles J. Multi-path Control Structures for Programming Languages. Ph.D. thesis. Harvard University, Cambridge, Mass., 1972.|
.ref chucksigplan,Prenner#73,|Prenner, Charles J. Extensible Control Structures. $SIGPLAN Notices 8$, 9 (September 1973), 129-132.|
.ref bensthesis,Wegbreit#70,|Wegbreit, Ben. Studies in Extensible Programming Languages. Ph.D. Thesis. Harvard University, Cambridge, Mass., May 1970.|
.ref EL1paper,Wegbreit#74,|Wegbreit, Ben. The Treatment of Data Types in EL1. $Comm. ACM 17$, 5 (May 1974), 251-264.|
.portion titlepage
.select sectionheadfont
.begin "titlepage"
.nofill center
.group skip 9
Generation of Optimized
Semaphore Synchronization Code
.skip 3
A thesis presented
.skip
by
.skip
Guy Lewis Steele Jr.
.skip
to
.skip
The Committee on Applied Mathematics
.skip
in partial fulfillment of the honors requirements
for the degree of
.skip
Bachelor of Arts
.skip 4
Harvard College
.skip
Cambridge, Massachusetts
.skip
May 1975
.end "titlepage"
.insert contents
.portion textbody
.select textfont
.count page to 999
.odd heading(%5↓_{chaptertitle},,Page {page!}_↓)
.odd footing(%5↓_{sectiontitle},,{sectionnumber}_↓)
.even heading(%5↓_Page {page!},,{chaptertitle}_↓)
.even footing(%5↓_{sectionnumber},,{sectiontitle}_↓)
.chapter chapintro,Introduction
This thesis presents some techniques for
generating reasonably good semaphore synchronization
code from the output of the SAL synthesizer,
which from assertions expressed in SAL, a very-high-level
language, generates high-level-language synchronization
code expressed in terms of Prenner's Control
Interpreter primitives.
While an attempt has been made to make this thesis
reasonably self-contained, the reader would do
well to be familiar with the contents of
[{patsthesis}] and [{chuck}], and with the semantics
of semaphores (see for example [{genuys}]).
The techniques presented here have not yet been
embodied in a working system for lack of time,
but have been hand-executed on a number of examples,
some of which will be presented in detail in
chapter @chapexamples@.
.chapter chapbackground,Background and Overview
.section backmotivation,Motivation
The motivation behind the work presented in this thesis
is the desire for a system which will ease the specification
of large, synchronized, multiple-process systems. We would
like to express such specifications in a very high-level language,
independent of any particular machine implementation;
the system should then translate the high-level specifications
into low-level code which will run on actual computers.
In order to accomplish this, we may separate the problem
into two portions: (1)#the problem of designing the specification
language, and (2)#the problem of translating the specifications.
This latter portion itself divides naturally into two parts:
(2a)#the problem of parsing and correlating
the specifications in relevant ways, and (2b)#the problem of
generating actual code.⊗⊗This separation is very similar
to that used in ordinary high-level language compilers.
For example, the MacLISP compiler [{moon}] is organized into two
passes, of which the first analyzes the input, correlating type
declarations, variable bindings, etc., and the second generates
and optimizes the machine-language code.⊗
Griffiths [{synver}] [{salpaper}] [{patsthesis}]
has done much work towards solving problems (1) and
(2a). She has designed a synchronization assertion language (SAL)
in which to express the synchronization properties of a system
of programs, and has built a translator
(the SAL synthesizer) which analyzes the
assertions and produces a kind of medium-level code expressed
in terms of Prenner's Control Interpreter Model. [{chuck}]
[{chucksigplan}]
This code should indeed run on such systems as have implemented
the CI primitives; however, at present only the ECL [{eclmanual}]
programming system at Harvard actually contains such
an implementation. For this reason the SAL synthesizer
and verifier are presently implemented in the ECL
programming system. The SAL assertion language is defined
in terms of extensions to the
EL1 extensible language which the ECL system supports.
The purpose of this thesis is to present a collection
of techniques for generating code expressed in terms of Dijkstra's
εPε and εVε semaphore primitives. [{genuys}] [{THEsystem}]
These techniques could
easily be used to construct a rear-end code generator for
use in conjunction with Griffiths' translation system;
one would then have a total system which would accept
SAL assertions and produce semaphore code.
This would thus achieve our original goal quite nicely, since
the εPε and εVε operations are quite easily implemented
in almost any modern computing environment, whether
multiple-processor or timeshared single-processor.
We would then have a total programming system which
looked something like this:
.begin "system picture" group
.select eclfont
.nofill
.tabs 25,45
------------------
| English |
|----------------|
| original |
| system |
| specifications |
------------------ -------------
| | user |
(|)---------------------------| (probably |
α↓ | human) |
------------------- -------------
| SAL (very high |
| level language) |
|-----------------|
| code using SAL |
| assertions |
------------------- -------------------
| | SAL synthesizer |
(|)------------------------| and verifier |
α↓ | (Griffiths) |
------------------------- -------------------
| ECL system with CI |
| (high level language) |
| (Prenner) |
|-----------------------|
| EL1 code using |
| CI primitives |
------------------------- ------------------
| | semaphore code |
(|)-------------------------| generator |
α↓ | (Steele) |
--------------------------- ------------------
| EL1 and semaphores |
| (medium level language) |
|-------------------------|
| EL1 code using |
| semaphore primitives |
--------------------------- ---------------
| | EL1 |
(|)--------------------------| compiler |
α↓ | (Holloway) |
-------------------- ---------------
| ECL system |
|------------------|
| machine language |
--------------------
.end "system picture"
The remainder of this chapter presents $very$ briefly
the background on EL1, CI, SAL, and semaphores
needed for proper understanding of the rest of the thesis.
For more complete descriptions [{eclmanual}], [{chuck}], [{patsthesis}],
and [{genuys}] should be consulted.
.section backecl,The EL1 Programming Language
↓_%5Warning:%*_↓
this section is meant to provide only a brief
tutorial on the features of the EL1 language used in
this thesis. It does not purport by any means to be a complete
description.
The EL1 language [{bensthesis}] [{EL1paper}] [{eclmanual}]
is a language which is Algol-like
in syntax, but LISP-like in semantics. Furthermore it provides
for user extensibility of both syntax and semantics;
it is by means of this facility, for example, that the SAL
language constructs are defined.
The extension features of the language will not be described here;
it is sufficient for the reader to be aware of their existence.
The specific extensions which SAL uses will be described
in section @backsal@.
EL1 programs are written free-form;
spaces and carriage returns may be included freely,
except that they may not be embedded in names of
variables and other identifiers. (In this thesis
EL1 code will always be presented in a nicely
indented form for readability.)
The EL1 language provides for both functional
and program statement structure. Function calls are written
in the usual Algol-like manner, i.e. the function name followed
by the arguments in parentheses and separated by commas.
Some functions are infix in syntax: thus one may write
/FOO#+#BAR/, which is entirely equivalent to /+(FOO,#BAR)/.
We shall use only very simple built-in functions,
plus two functions on semaphores. All of them except the semaphore
functions may be written as prefix or infix operators as appropriate.
They are (in decreasing order of precedence):
.beginecl
.tabs 8
.select textfont
%3IE%*↑comment (prefix function, ignores argument)
%3*%*↑integer multiplication
%3α/%*↑integer division
%3+%*↑integer addition
%3-%*↑integer subtraction or unary negation
%3NOT%*↑Boolean not (/TRUE/ if and only if argument is /FALSE/)
%3=%*↑equality (/TRUE/ if and only if arguments have same mode and value)
%3α#%*↑inverse of %3=%*
%3GT%*↑greater than (compares integers)
%3GE%*↑greater or equal (compares integers)
%3LT%*↑less than (compares integers)
%3LE%*↑less or equal (compares integers)
%3AND%*↑Boolean and (/TRUE/ if and only if both arguments are /TRUE/)
%3OR%*↑Boolean or (/TRUE/ if and only if either argument is /TRUE/)
εPε↑the εPε-operation on semaphores
εVε↑the εVε-operation on semaphores
.endecl
Statement structure is provided by /BEGIN#...#END/
blocks containing statements separated by semicolons.
A statement may be any expression. The value of a block
is the value of the last expression in the block
(see, however, the description of the /=>/ construct below);
the other statements in a block are useful only for side
effects such as assignment or subroutine calls.
The two tokens /[)/ and /(]/ are entirely equivalent to
/BEGIN/ and /END/, and will also be used in this thesis.
Variables are written as strings of letters and digits
in the usual manner. The character "%3\%*" may also be
part of the name of a variable. Every variable has
a type, called its $mode$; we will need only the standard modes
/INT/ (integers) and /BOOL/ (Boolean, i.e. of value
/TRUE/ or /FALSE/), and also the special mode
/SEMAPHORE/ (variables to which the εPε and εVε operations
may be applied). For our purposes we will
consider all variables to be global.
Values may be assigned to variables by using the
↓_∀←_↓ operator. Thus /FOO#/↓_∀←_↓/#43/ assigns
the value /43/ to the variable /FOO/.
There are two kinds of conditionals: /=>/ and /->/.
The /=>/ conditional may be used only as a "statement"
of a /BEGIN#...#END/ block; in such a position the
statement /FOO#=>#BAR/ means that if /FOO/ evaluates to
/TRUE/, then the value of the block is the value of
/BAR/, and no more statements are executed.
If /FOO/ evaluates to /FALSE/, then /BAR/ is not evaluated,
but rather the following statements in the block.
The other conditional, /->/, may be used anywhere.
The value of the expression /FOO#->#BAR/ is the value of
/BAR/ if the value of /FOO/ is /TRUE/, and otherwise
/NOTHING/ (a special "null constant").
Thus /FOO#->#BAR/ is the same as:
.beginecl
[) FOO => BAR; NOTHING (]
.endecl
A variant of /BEGIN#...#END/ is /REPEAT#...#END/,
which has the effect of repeatedly executing its contained
statements in cyclic order, the first following the last.
The /=>/ construct may be used to exit such a loop.
Functions are defined by means of the /EXPR/
construct. We will be defining only functions of zero
arguments, and so it suffices to state that
a function constant of no arguments is written as:
.beginecl
EXPR()body\of\function
.endecl
where /body\of\function/ is any EL1 expression.
A name is given to a function by assigning the function
constant to a variable with a functional mode:
.beginecl
TRIPLE\FOO ∀← EXPR()(FOO ∀← FOO * 3);
.endecl
Angle brackets /<#...#>/ enclose a number
of expressions separated by commas, and represent a
quoted list of those expressions.
.section backci,The Control Interpreter
↓_%5Warning:%*_↓ this does not purport by any means to
be a complete description of the Control Interpreter
synchronization model. For a complete description, see [{chuck}] or [{chucksigplan}].
The CI system provides a primitive /CIA/
("↓_C_↓ontrol ↓_I_↓nterpreter ↓_A_↓pply")
which takes a function as its
argument. This primitive has two properties which make it
useful for synchronization.
(1) The function is invoked in a special environment, namely
that of the Control Interpreter, and so the function has
access to variables which are preserved between /CIA/
invocations and which are otherwise inaccessible.
(2) Any two invocations of /CIA/ by any two processes
are mutually exclusive in time; thus only one process may
access the Control Interpreter's environment at a time.
The order in which processes contending for
the privilege of using the /CIA/ primitive are
serviced is purposely left undefined.⊗⊗In fact,
it would be meaningless to define such an order,
though that will not be proved in this thesis.⊗
There are two special variables in the Control
Interpreter's environment: /LASTRUN/ and
/INACTIVEQ/. The latter is a queue of
process descriptors for processes which are in a
runnable state but are not actually running;
a process can be scheduled to run by putting it in
/INACTIVEQ/, which a hidden scheduler
is presumed to examine at every clock tick and run
processes from. The variable /LASTRUN/
contains, on entry to the Control Interpreter's
environment, the descriptor for the process that
invoked the Control Interpreter (by using /CIA/).
On exit from the Control Interpreter, /LASTRUN/
should contain either the process descriptor for the
next process to be scheduled
(possibly the same one), or /NIL/, which means that
some process from /INACTIVEQ/ will eventually
be scheduled.
There are two functions available for
manipulating queues: /REMOVEF/ and /ENTERL/.
The former removes an item from the front of a queue,
and the latter enters an item as the last item in a queue.
An empty queue is equal to /NIL/ and so the
expression /RANDOM\QUEUE#=#NIL/ is /TRUE/
if and only if the queue /RANDOM\QUEUE/ is empty.
As an example of the use of the Control
Interpreter, consider these definitions of two concurrent
processes:
.beginecl
PRODUCER ∀← EXPR()
↑REPEAT
↑↑IE "THIS ROUTINE PRODUCES THINGS";
↑↑CIA("PRODUCER\BUFFER\WAIT");
↑↑BUFFER ∀← PRODUCE\ITEM();
↑↑CIA("PRODUCER\BUFFER\RELEASE");
↑END;
.endecl
.beginecl
CONSUMER ∀← EXPR()
↑REPEAT
↑↑IE "THIS ROUTINE CONSUMES THINGS";
↑↑CIA("CONSUMER\BUFFER\WAIT");
↑↑CONSUME\ITEM(BUFFER);
↑↑CIA("CONSUMER\BUFFER\RELEASE");
↑END;
.endecl
Let there be a variable in the Control Interpreter's
environment called the "empty flag".
The producer waits for the buffer to become empty,
fills the buffer, then releases it by clearing an empty flag.
The consumer waits for the buffer to become full, empties
the buffer, then releases it by setting the empty flag.
We can implement this by defining the four functions
for the /CIA/ invocations as follows:
.beginecl
PRODUCER\BUFFER\WAIT ∀← EXPR()
↑BEGIN
↑↑BUFFER\EMPTY => NOTHING;
↑↑WAITING\PRODUCER ∀← LASTRUN;
↑↑LASTRUN ∀← NIL;
↑END;
.endecl
.beginecl
PRODUCER\BUFFER\RELEASE ∀← EXPR()
↑BEGIN
↑↑BUFFER\EMPTY ∀← FALSE;
↑↑WAITING\CONSUMER α# NIL ->
↑↑ [) ENTERL(WAITING\CONSUMER, INACTIVEQ);
↑↑ WAITING\CONSUMER ∀← NIL (];
↑END;
.endecl
.beginecl
CONSUMER\BUFFER\WAIT ∀← EXPR()
↑BEGIN
↑↑NOT BUFFER\EMPTY => NOTHING;
↑↑WAITING\CONSUMER ∀← LASTRUN;
↑↑LASTRUN ∀← NIL;
↑END;
.endecl
.beginecl
CONSUMER\BUFFER\RELEASE ∀← EXPR()
↑BEGIN
↑↑BUFFER\EMPTY ∀← FALSE;
↑↑WAITING\PRODUCER α# NIL ->
↑↑ [) ENTERL(WAITING\PRODUCER, INACTIVEQ);
↑↑ WAITING\PRODUCER ∀← NIL (];
↑END;
.endecl
Note that in the above definitions, if either process has to
wait, it puts its descriptor in a well-known place and sets
/LASTRUN/ to /NIL/ (after all, there might be
yet other processes in the system to schedule).
The other process will eventually put it back on
/INACTIVEQ/ when it releases the buffer.
.section backsal,The Synchronization Assertion Language
The SAL language allows the specification
of the synchronization properties of a system of programs
in terms of non-procedural $state assertions$ placed
at certain points in the code.
It is based to a great extent on the Control Interpreter
synchronization mechanism.
The code for each program is written with /CIA/
invocations wherever synchronization is required;
however, the code to be executed in the Control
Interpreter is $not$
specified. Instead, state assertions are placed
before and after each /CIA/ invocation.
These assertions reflect the changes in the total
state of the system which the /CIA/ invocation is
to implement. The SAL synthesizer analyzes these
assertions and produces functions which when run in the
Control Interpreter
will cause the declared state changes to occur.
.subsec salformat,Format of SAL Program Specifications
A system of programs is specified in the following
manner:
.beginecl
<↑state1 IS expression1,
↑state2 IS expression2,
↑... ,
↑statem IS expressionm,
↑process1 DOES codebody1,
↑process2 DOES codebody2,
↑... ,
↑processn DOES codebodyn >
.endecl
The /statei/ and /processi/ are identifying names.
The /expressioni/ are Boolean expressions in terms
of one or more state variables.
For example:
.beginecl
<↑IDLE IS BUSY = 0 AND DONE = 1,
↑STARTED IS BUSY = 1 AND DONE = 0,
↑FINISHED IS BUSY = 1 AND DONE = 1,
↑HUNG IS BUSY = 0 AND DONE = 0,
↑...
.endecl
The /codebodyi/ are bodies of code which contain
/CIA/ invocations
surrounded by SAL assertions.
As an example:
.beginecl
↑CPU DOES
↑↑BEGIN
↑↑↑ASSERT(IDLE, STARTED, FINISHED, HUNG);
↑↑↑CIA("START\UP\DEVICE");
↑↑↑ASSERT(IDLE ==> STARTED, ELSE WAIT);
↑↑↑...
↑↑↑ASSERT(STARTED, FINISHED, HUNG);
↑↑↑CIA("NEED\DATA");
↑↑↑ASSERT(FINISHED ==> IDLE, ELSE WAIT);
↑↑END
.endecl
Each process specified is generally assumed
to be cyclic (i.e. repeatable).⊗⊗In fact the SAL verifier
can determine whether the code indeed has this property.⊗
.subsec salassertions,SAL Assertions
The assertions preceding each CIA are $invariant assertions$;
they mention all the states which the total
system could be in when the CI is to be invoked at that point.
The assertions following each CIA are $result assertions$;
they indicate the state transitions which the invocation
of the CI may cause. Thus in the example above, before the
second CIA the system is declared not to be in the /IDLE/
state, since the "device" has been started up;
the /CPU/ process is furthermore declared to wait
unless the "device" has put the system into the finished state
(which it will presumably do eventually, since the CPU put
the system into the /STARTED/ state).
A result transition is generally of the form:
.beginecl
old\state ==> new\state AND actions
.endecl
where /actions/ may be of various kinds which are described
below. The /old\state/ may be further constrained by
a Boolean expression; for example:
.beginecl
READING AND NUMBER\OF\READERS GT 43 ==> WEDGED
.endecl
As a further convenience, both /old\state/ and /new\state/
may be lists of states. For example:
.beginecl
<IDLE, STARTED> ==> <STARTED, HUNG> AND actions
.endecl
may be written instead of the more tedious:
.beginecl
IDLE ==> STARTED AND actions,
STARTED ==> HUNG AND actions
.endecl
The construction:
.beginecl
ELSE new\state ...
.endecl
may be used as the last transition in a result assertion;
the keyword /ELSE/
represents all old states in the invariant
assertion which were not explicitly accounted for
in the previous transitions.
The keyword /ALWAYS/ may be used instead of /ELSE/ if the /ELSE/-transition
is the only transition.
All the /old\state/s mentioned in the transitions
of a result assertion must be mutually exclusive,
and their union must cover the states mentioned in the
preceding invariant assertion.
For example:
.beginecl
↑ASSERT(READING, SLEEPING);
↑CIA("SLEEP\IF\ONLY\READER\OR\ALREADY\SLEEPING");
↑ASSERT(SLEEPING ==> SLEEPING,
↑ READING AND NUMBER\OF\READERS = 1 ==> SLEEPING,
↑ READING AND NUMBER\OF\READERS α# 1 ==> READING);
.endecl
Thus all states are accounted for,
and there is no ambiguity as to the action the CI function
should take. Note that states ordinarily notated as single names
may be "split" in such transition assertions by the use
of Boolean expressions, but these expressions must also
be disjoint and together cover all possibilities.
.subsec salwaitsets,Waitsets
In order to have a means of expressing the delays
a process may encounter because of mutual exclusion,
the notion of $waitsets$ is used in SAL.
A waitset is an unordered set of
processes which are not permitted
to proceed with their execution, and are therefore
in a suspended state.
Typically, when a process determines within a CI function
that the system state is such that it connot usefully
proceed, it places itself in a waitset, from which some
other process will presumably eventually revive it.
No process may belong to more than one waitset at any
given time.
.subsec salactions,Result Assertion Actions
In order to use the waitsets, various actions
are specified in the result assertions in addition
to each of the various state transitions.
Zero or more actions may appear on the right-hand side
of a result transition after the specified /new\state/;
they are separated by the keywords /AND/ and /THEN/.
The keyword /AND/ specifies unordered conjunction,
and the keyword /THEN/ specifies ordered conjunction.
.subsubsec actionwait,The /WAIT/ Action
This action specifies that the current process is
to wait in a waitset. The waitset may be explicitly
specified by saying:
.beginecl
↑WAIT IN waitset\name
.endecl
or implicitly specified by saying merely:
.beginecl
↑WAIT
.endecl
The name of such an implicitly specified waitset is the same as the
name of the waiting process.
.subsubsec actionstartup,The /STARTUP/ Action
This action is used to remove another process from
a waitset and let it proceed. The basic form is:
.beginecl
↑STARTUP(process\name OUTOF waitset\name)
.endecl
which selects some process in the waitset and allows
it to proceed. That process will then execute the
next statement after the /CIA/ invocation which caused
it to perform a /WAIT/.
If the keyword /ALL/ precedes the
/process\name/, then $all$ processes in the waitset are
allowed to proceed. If the phrase /OUTOF#waitset\name/
is omitted, the implicit waitset for processes with the
name /process\name/ is used.
.subsubsec actionrevive,The /REVIVE/ Action
When a process uses a /STARTUP/ in a result transition
to allow another process to proceed, it is the responsibility
of that transition to put the system into the correct
global state for the other process to proceed in.
This means, however, that each process must know something
about the states the other processes expect.
An alternative is provided by the /REVIVE/ contruct.
This is identical to /STARTUP/, except that the keyword /STARTUP/
is replaced by /REVIVE/.
The semantics of /REVIVE/ are that when a process is removed
from a waitset, the entire result assertion of the waiting process
is used to determine a new state transition (and possibly further
actions). It is as if the waiting process were allowed to proceed
by $repeating$ its /CIA/ call in the (now altered) state of the system,
rather than by proceeding from $after$ the /CIA/ call.
In this way the state information for a process is more easily
kept local to the assertions of that process.
Note that the result assertion of the revived process takes effect $before$
any other process gets into the CI; we may think of this as
explicitly "passing the mutual exclusion" from one process
to another (see [{hoare}]).
The /REVIVE/ action is normally preceded by /THEN/ rather than
/AND/ since the assertion of the revived process should not
be examined until the currently specified transition
has been effected.
.subsubsec actiontry,The /TRY/ Construct
It is often desirable to test a number of alternatives
in some priority order and perform the first one, if any, which
is possible. (For example, one might want to let a writer into
a data base if one is waiting, and otherwise let a reader proceed.)
The /TRY/ construct provides such a priority ordering.
It may be written in place of an action on the right-hand side
of a result transition, and has the following form:
.beginecl
↑TRY IF actions1 POSSIBLE
↑NEXT IF actions2 POSSIBLE
↑...
↑NEXT IF actionsn POSSIBLE
↑END\TRY
.endecl
The semantics of /TRY/ are that if it is possible to
perform /actions1/, then those actions are performed;
otherwise, if /actions2/ are possible, then those are performed; ...
otherwise, if /actionsn/ are possible, then those are
performed; otherwise, no actions are performed.
Note that a /STARTUP/ or /REVIVE/ is considered possible if and only if
there is at least one process in the specified waitset.
In particular, /STARTUP(ALL ...)/ or /REVIVE(ALL ...)/ are
possible if and only if there is at least one process
in the waitset.
Normally a /TRY/ construct is preceded by /THEN/ since
the ordering of a /TRY/ with respect to other actions
is important. Also, the actions specified in a /TRY/
are normally /STARTUP/s and /REVIVE/s.
.subsubsec actioneither,The /EITHER/ Construct
Sometimes it is desirable to choose among some
alternatives without any priority and perform any one
alternative.
(For example, one might want to let a writer or a reader
into the data base next, but not both at once, and with
indifference as to priority.)
For this purpose the /EITHER/ construct is provided.
It chooses an arbitrary action sequence from a set of
such sequences and performs the selected actions.
The form is:
.beginecl
↑EITHER actions1
↑ OR actions2
↑ ...
↑ OR actionsn
↑END\OR
.endecl
If the /EITHER/ construct is not embedded within a /TRY/
construct, then all the action sequences are assumed
possible, and whichever one is chosen will be executed.
If the /EITHER/ construct is embedded within a /TRY/ construct,
then it has a slightly different interpretation:
it specifies several alternatives to be tried with equal priority.
For example:
.beginecl
↑TRY IF actions1 POSSIBLE
↑NEXT EITHER IF actions2a POSSIBLE
↑ OR IF actions2b POSSIBLE
↑ OR IF actions2c POSSIBLE
↑ END\OR
↑NEXT IF actions3 POSSIBLE
↑END\TRY
.endecl
will perform /actions1/ if possible;
otherwise if any of /actions2a/, /actions2b/, /actions2c/
are possible then it will perform one of the possible sequences;
otherwise it will perform /actions3/ if possible;
otherwise it will do nothing.
For example, one might write the following result assertion
for a data base program:
.beginecl
↑ASSERT(LOCKED ==> UNLOCKED THEN
↑ TRY EITHER IF REVIVE(WRITER) POSSIBLE
↑ OR IF REVIVE(ALL READER) POSSIBLE
↑ END\OR
↑ NEXT IF REVIVE(LOW\PRIORITY\READER) POSSIBLE
↑ END\TRY);
.endecl
That is, within a /TRY/ construct, each possible choice
of an embedded /EITHER/ construct must be considered
and rejected as not possible before the next lower priority
case of the /TRY/ may be considered. On the other hand,
when not embedded within a /TRY/, the /EITHER/ construct
makes one choice and performs it, even if performing
it is a null operation (such as /STARTUP(ALL ...)/
on an empty waitset).
.subsec salexample,Example of the Use of SAL
As an example of the use of SAL, let us consider
a solution to the "first readers and writers" problem [{courtois}].
(This example will be used later in section @readers@.)
Suppose that we have a data base, and two classes
of processes known as $readers$ and $writers$.
Suppose furthermore that any number of readers may read
from the data base simultaneously, but if a writer is
writing then no other process may access the data base.
Furthermore assume that neither readers nor writers are
to receive any particular priority.
The system as we have defined it has three
significant states: the quiescent state, the state where one
or more readers are reading, and the state where a writer
is writing. Let us call these states /QUIESCENT/, /READING/,
and /WRITING/.
We can reflect these states in two state variables;
let us call them /NUMBER\OF\READERS/ and /WRITE\FLAG/,
with the obvious semantics.
We will need two waitsets: one for waiting readers,
and another for waiting writers. Let us call them
/READER\QUEUE/ and /WRITER\QUEUE/.
We may then encode a solution to our problem in
SAL as follows:
.beginecl
<↑QUIESCENT IS WRITER\FLAG = FALSE
↑↑↑↑AND NUMBER\OF\READERS = 0,
↑READING IS WRITER\FLAG = FALSE
↑↑↑↑AND NUMBER\OF\READERS GT 0,
↑WRITING IS WRITER\FLAG = TRUE
↑↑↑↑AND NUMBER\OF\READERS = 0
↑READER DOES
↑↑BEGIN
↑↑↑ASSERT(QUIESCENT, READING, WRITING);
↑↑↑CIA("START\READ");
↑↑↑ASSERT(<QUIESCENT, READING> ==> <READING, READING>,
↑↑↑ ELSE WAIT IN READER\QUEUE);
↑↑↑IE "READ FROM DATA BASE";
↑↑↑ASSERT(READING);
↑↑↑CIA("END\READ");
↑↑↑ASSERT(READING AND NUMBER\OF\READERS GT 1 ==> READING,
↑↑↑ READING AND NUMBER\OF\READERS = 1 ==>
↑↑↑↑↑↑QUIESCENT THEN
↑↑↑↑↑↑TRY IF REVIVE(WRITER) POSSIBLE END\TRY);
↑↑END,
↑WRITER DOES
↑↑BEGIN
↑↑↑ASSERT(QUIESCENT, READING, WRITING);
↑↑↑CIA("BEGIN\WRITE");
↑↑↑ASSERT(QUIESCENT ==> WRITING,
↑↑↑ ELSE WAIT IN WRITER\QUEUE);
↑↑↑IE "WRITE INTO DATA BASE";
↑↑↑ASSERT(WRITING);
↑↑↑CIA("END\WRITE");
↑↑↑ASSERT(ALWAYS QUIESCENT THEN
↑↑↑ TRY EITHER IF REVIVE(ALL READER
↑↑↑ OUTOF READER\QUEUE)
↑↑↑ POSSIBLE
↑↑↑ OR IF REVIVE(WRITER
↑↑↑ OUTOF WRITER\QUEUE)
↑↑↑ POSSIBLE
↑↑↑ END\OR
↑↑↑ END\TRY);
↑↑END >
.endecl
Note the usage of /ELSE/ and /ALWAYS/ in the result assertions,
and also the usage of /EITHER/ to indicate the lack of priority
ordering on the instances of /REVIVE/.
Note too that by using /REVIVE/ a process need know nothing
about the intentions of the process or processes being revived,
but need merely return the system to the /QUIESCENT/ state before
reviving the other process or processes.
.section backsemaphores,Semaphore Synchronization
Semaphores were originally defined by Dijkstra [{genuys}]
for the purpose of synchronizing otherwise
asynchronous processes.
He defines semaphores and their behavior as follows:
.begin "temp1"
.narrow 4,5
.indent 0,6
.skip 1
The semaphores are essentially non-negative integers.
$Definition.$ The εVε-operation is an operation
with one argument, which must be the identification of
a semaphore. (If "S1" and "S2" denote semaphores we can
write "εVε(S1)" and "εVε(S2)".) Its function is to
increase the value of its argument semaphore by 1; this increase
is to be regarded as an indivisible operation.
$Definition.$ The εPε-operation is an operation
with one argument, which must be the identification of
a semaphore. (If "S1" and "S2" denote semaphores we can
write "εPε(S1)" and "εPε(S2)".) Its function is to
decrease the value of its argument semaphore by 1 as soon as
the resulting value would be non-negative. The completion
of the εPε-operation -- i.e. the decision that this is
the appropriate moment to effectuate the decrease and the
subsequent decrease itself -- is to be regarded as an
indivisible operation.
.skip 1
.end "temp1"
.next page << fix losing footnote problem >>
.continue
Now these definitions seem to be perfectly straightforward;
indeed it is their apparent simplicity which makes semaphores
so widely used in solutions of synchronization problems.
It should be remembered, however, that no ordering of any
kind is specified,⊗⊗As for the Control Interpreter,
depending on the order of success of εPε-operations
is actually erroneous, and it would be nonsensical to
define such an ordering. On the other hand, it would not be
incorrect to $implement$ semaphores in terms of some queuing
mechanism, as long as no program tried to "take advantage"
of the fact that the semaphores were so implemented.⊗
nor is it specified exactly how a process
is kept suspended if a εPε-operation cannot succeed
immediately.
For the purposes of this thesis it will not be necessary
to go into the internal details of the implementation
of semaphores. As an example, however, we may consider here
an implementation of the εPε and εVε operations
in terms of the Control Interpreter primitives.
Let us assume that in order to perform ↓_εPε_↓/(S43)/
that we are willing to say:
.beginecl
↑CIA("P43");
.endecl
and similarly to perform ↓_εVε_↓/(S43)/ we will say:
.beginecl
↑CIA("V43");
.endecl
Then we may define the functions /P43/ and /V43/
as follows:
.beginecl
P43 ∀← EXPR()
↑BEGIN
↑↑IE "IF > 0, DECREMENT AND EXIT";
↑↑S43 GT 0 => S43 ∀← S43 - 1;
↑↑IE "OTHERWISE PUT SELF ON QUEUE";
↑↑ENTERL(LASTRUN, S43\QUEUE);
↑↑LASTRUN ∀← NIL;
↑END;
V43 ∀← EXPR()
↑BEGIN
↑↑IE "IF NOBODY WAITING, INCREMENT AND EXIT";
↑↑S43\QUEUE = NIL => S43 ∀← S43 + 1;
↑↑IE "OTHERWISE START SOMEONE UP";
↑↑ENTERL(REMOVEF(S43\QUEUE), INACTIVEQ);
↑END;
.endecl
Thus, any processes waiting to complete a εPε-operation
place themselves on a queue, to be released by a subsequent
εVε-operation.
.chapter chapbrute,Straightforward Brute Force Translation
↓_%5Warning:%*_↓
the methods outlined in this chapter
are ↓_$not correct$_↓.
There is a slight problem which will
be discussed in chapter @chapmutex@. The incorrect
solution is presented first in order to give some historical
insight, as well as to make clear the subtle nature of the
problems which can arise in the domain of process
synchronization.
We wish to take the output of the SAL
synthesizer, which is expressed in terms of Control
Interpreter primitives, and from it generate code
which uses semaphore primitives. In order to do this
we must model the behavior of waitsets in terms of
semaphores, and specify the translation of the various
SAL constructs in terms of semaphores as well.
(We shall assume that the generator has available to
it the original SAL code and any data about the code
derived by the SAL synthesizer and verifier, as well
as the synthesized CI code itself.)
The translation methods outlined in this chapter
are quite straightforward and "brute-force" in nature.
It will be seen that the code produced, though operational,
leaves much to be desired in terms of the amount of code used
to accomplish the task, as compared, say, with the amount of
code a reasonably competent human programmer might
produce. This problem will be dealt with
in chapter @chapoptimize@.
.section brutestrategy,General Translation Strategy
The synchronization functions produced by
the SAL synthesizer contain two kinds of code:
code which directly reflects the result assertion actions,
such as /WAIT/ and /REVIVE/, and code
which effects the state changes by manipulating the
state variables. In order to produce code in terms
of semaphore primitives we will take the Control
Interpreter functions produced by the SAL
synthesizer and convert the first kind of code.
The second kind of code will be retained but not altered.
At the beginning of the function we will place a
tag (to which a /GOTO/⊗⊗Structured programmers
may suspect from this alone that something is wrong.
It will in fact be true that when we fix the bug
described in chapter @chapmutex@, the need for
the /GOTO/ will disappear. However,
the problem is not the presence of the /GOTO/,
but a subtle timing bug. The /GOTO/
could be eliminated here by use of nested /REPEAT/
loops, without even having to introduce auxiliary
variables, but the method is tedious and we will find
it easier to use the /GOTO/ for the nonce.
(Historical note: EL1 originally had the /GOTO/
statement, but it has since been declared harmful and
de-implemented from the ECL system.)⊗
may branch); this will
be used in translating /REVIVE/.
.subsec brutewaitset,Modelling Waitsets with Semaphores
For every waitset /FOO/ mentioned in the original
SAL assertions, we will introduce a semaphore
/FOO\SEM/; processes in the waitset will be
modelled as processes waiting to perform a εPε on the
semaphore. Additionally we will sometimes introduce
as associated counter /FOO\COUNT/, which will be
an integer variable used to keep track of the number
of processes in the waitset; this will be useful in translating
the /STARTUP/ and /REVIVE/ actions.
.subsec bruteci,Modelling /CI/ Exclusion Using /mutex/
In order to model the mutual exclusion implied by
the /CIA/ primitive, i.e. that no two synchronization
functions may be executed at the same time, we will introduce
an auxiliary semaphore /mutex/. At the beginning of
each synchronization function (just after the introduced
tag) we will place a ↓_εPε_↓/(mutex)/, and at the end
of each function we will place ↓_εVε_↓/(mutex)/.
If necessary, the latter operation must be split
and propagated backward through the arms of conditionals
so that any εPε operations generated by translation
of /WAIT/ actions (see section @primwait@),
and possibly any /GOTO/ statements generated by
translation of /REVIVE/ actions
(see section @primstartup@),
will follow and not precede the ↓_εVε_↓/(mutex)/.
.next page << footnote loss >>
.section bruteprim,Translation of SAL Primitives
The translation of the /WAIT/ actions
and the translation of the /STARTUP/ and
/REVIVE/ actions are intimately related.
In order to accomplish the translations
we will need to impose the restriction
that, in the SAL assertions for a system,
a given waitset may not have both /STARTUP/
and /REVIVE/ used on it.⊗⊗The SAL
synthesizer supports this restriction. It turns out
that in practice this is not very confining;
no actual problem tried so far in SAL assertions
has required the use of both /STARTUP/
and /REVIVE/ on a single waitset.
On the other hand, we will eventually be able to
lift this restriction in section @extractstrategy@.⊗
.subsec primwait,Translation of /WAIT/
We will translate the /WAIT/ action
in one of four ways, depending on two conditions:
(1) whether /STARTUP/ or /REVIVE/
is used on it, and (2) whether or not one of the
/ALL/ or /IF#...#POSSIBLE/
constructs is ever used on the waitset.
Suppose, for instance, that we wish to translate
the action:
.beginecl
WAIT IN FOO
.endecl
where /FOO/ is a waitset. Suppose that /TAG27/
is the tag at the top of the synchronization function
in which the /WAIT/ action appears.
Then the translation of the action into semaphore
primitives may take one of four forms:
.skip continue
(1) /STARTUP/ is used, but not /ALL/ or
/IF#...#POSSIBLE/:
.beginecl
↑↑↑↑εPε(FOO\SEM)
.endecl
(2) /REVIVE/ is used, but not /ALL/ or
/IF#...#POSSIBLE/:
.beginecl
↑↑↑↑[) εPε(FOO\SEM);
↑↑↑↑ GOTO TAG27 (]
.endecl
(3) /STARTUP/ is used, and also /ALL/ or
/IF#...#POSSIBLE/:
.beginecl
↑↑↑↑[) FOO\COUNT ∀← FOO\COUNT + 1;
↑↑↑↑ εPε(FOO\SEM) (]
.endecl
(4) /REVIVE/ is used, and also /ALL/ or
/IF#...#POSSIBLE/:
.beginecl
↑↑↑↑[) FOO\COUNT ∀← FOO\COUNT + 1;
↑↑↑↑ εPε(FOO\SEM);
↑↑↑↑ GOTO TAG27 (]
.endecl
Thus, the use of
/REVIVE/ on a waitset necessitates the presence
of a /GOTO/ in the translation of any /WAIT/
action on that waitset, in order that the revived process
may re-execute its synchronization function;
similarly, the use of /ALL/
or /IF#...#POSSIBLE/ necessitates the updating
of an associated counter which is used to determine how
many processes are in the waitset.
.subsec primstartup,Translation of /STARTUP/ and /REVIVE/
The translations of the /STARTUP/
and /REVIVE/ actions into semaphore primitives
are identical. This is reasonable since the distinction
between the two is reflected in the translation
of the /WAIT/ actions.
For this reason, /STARTUP/ and /REVIVE/
will be treated as identical for the rest of this
chapter; unless they are specifically distinguished,
any mention of /STARTUP/ will apply also to
/REVIVE/.
There will be two ways to translate /STARTUP/,
depending on whether the /ALL/ or
/IF#...#POSSIBLE/ constructs are ever used
on the waitset in question, whether in the /STARTUP/
under consideration or in any other /STARTUP/.
Suppose that the action to be translated is:
.beginecl
STARTUP(PROCESS OUTOF FOO)
.endecl
Then the two possible translations are as follows:
.break continue
(1) /ALL/ and /IF#...#POSSIBLE/ are
not used on the waitset.
.beginecl
↑↑↑↑εVε(FOO\SEM)
.endecl
(2) /ALL/ and /IF#...#POSSIBLE/ are
used on the waitset.
.beginecl
↑↑↑↑[) FOO\COUNT ∀← FOO\COUNT - 1;
↑↑↑↑ εVε(FOO\SEM) (]
.endecl
Thus, as for /WAIT/, the associated counter must be
updated if the /ALL/ or /IF#...#POSSIBLE/
constructs are used on the waitset.
.subsec primall,|Translation of /STARTUP(ALL ...)/|
The translation of /STARTUP(ALL#...)/
is quite straightforward, given the translation of an
ordinary /STARTUP/;
it is merely necessary to write a loop
which will release all waiting processes from a waitset.
This implies performing a εVε operation enough
times to account for all εPε operations which have been
performed by waiting processes.
Thus we may translate this action:
.beginecl
STARTUP(ALL PROCESS OUTOF FOO)
.endecl
as the following "canned" loop:⊗⊗The SAL synthesizer in
fact uses just such a canned loop to translate
/STARTUP(ALL#...)/ into CI primtives.⊗
.beginecl
↑↑↑↑REPEAT
↑↑↑↑↑FOO\COUNT = 0 => NOTHING;
↑↑↑↑↑FOO\COUNT ∀← FOO\COUNT - 1;
↑↑↑↑↑εVε(FOO\SEM);
↑↑↑↑END
.endecl
The /=>/ conditional exits the loop when the count
reaches zero (which it may be initially), returning
the null value /NOTHING/.
Otherwise it decrements the counter, performs a εVε
on the semaphore, and loops around.
.subsec primifposs,Translation of /IF ... POSSIBLE/
Given the counter which keeps track of the size of a
waitset, it is easy to translate the necessary possibility
test into a test for equality with zero.
Thus we may translate the action:
.beginecl
IF STARTUP(PROCESS OUTOF FOO) POSSIBLE
.endecl
as the following conditional:
.beginecl
↑↑↑↑FOO\COUNT GT 0 ->
↑↑↑↑↑[) FOO\COUNT ∀← FOO\COUNT - 1;
↑↑↑↑↑ εVε(FOO\SEM) (]
.endecl
Similarly, this action:
.beginecl
IF STARTUP(ALL PROCESS OUTOF FOO) POSSIBLE
.endecl
may be translated as a loop within a conditional:
.beginecl
↑↑↑↑FOO\COUNT GT 0 ->
↑↑↑↑↑REPEAT
↑↑↑↑↑↑FOO\COUNT = 0 => NOTHING;
↑↑↑↑↑↑FOO\COUNT ∀← FOO\COUNT - 1;
↑↑↑↑↑↑εVε(FOO\SEM);
↑↑↑↑↑END
.endecl
It may be noted that the conditional is actually superfluous
in this case, but becomes necessary when the
/IF#...#POSSIBLE/ is translated in the
context of a /TRY/ construct.
.subsec primtry,Translation of /TRY ... END\TRY/
The /TRY/ construct is very much
like a LISP /COND/,
and so translates more or less naturally into a
/BEGIN#...#END/ block with conditional exits within it
for each possibility test.
Any /IF#...#POSSIBLE/ within a /TRY/ construct is translated
as already described in section @primifposs@, but with the
/->/ arrow replaced by a /=>/.
Thus, for example, the following construct:
.beginecl
TRY IF REVIVE(WRITER) POSSIBLE
NEXT IF REVIVE(ALL READER) POSSIBLE
NEXT IF REVIVE(LOW\PRIORITY\WRITER) POSSIBLE
END\TRY
.endecl
would translate into the following block:
.beginecl
↑↑↑↑BEGIN
↑↑↑↑↑WRITER\COUNT GT 0 =>
↑↑↑↑↑↑[) WRITER\COUNT ∀← WRITER\COUNT - 1;
↑↑↑↑↑↑ εVε(WRITER\SEM) (];
↑↑↑↑↑READER\COUNT GT 0 =>
↑↑↑↑↑↑REPEAT
↑↑↑↑↑↑↑READER\COUNT = 0 => NOTHING;
↑↑↑↑↑↑↑READER\COUNT ∀← READER\COUNT - 1;
↑↑↑↑↑↑↑εVε(READER\SEM);
↑↑↑↑↑↑END;
↑↑↑↑↑LOW\PRIORITY\WRITER\COUNT GT 0 =>
↑↑↑↑↑↑[) LOW\PRIORITY\WRITER\COUNT ∀←
↑↑↑↑↑↑↑ LOW\PRIORITY\WRITER\COUNT - 1;
↑↑↑↑↑↑ εVε(LOW\PRIORITY\WRITER\SEM) (];
↑↑↑↑END
.endecl
.subsec primeither,Translation of /EITHER ... OR ... END\OR/
In order to translate the /EITHER/ construct, we will
find it convenient to introduce a non-standard construct
into the EL1 language, which we shall call the /SELECT/
statement. It is quite similar to the existing EL1
/CASE/ statement
in structure (which was not described in section @backecl@
inasmuch as we will not need the /CASE/ statement
itself).⊗⊗The BNF for the /SELECT/
statement will not be presented here,
but it presumably would not be difficult to add to the
EL1 grammar; alternatively, we may think of it merely as
a convenient expository device for the purposes at hand.⊗
A /SELECT/ statement has the following form:
.beginecl
↑↑↑↑SELECT
↑↑↑↑↑[pred1] value1;
↑↑↑↑↑[pred2] value2;
↑↑↑↑↑...
↑↑↑↑↑[predn] valuen;
↑↑↑↑ELSE default\value
.endecl
The semantics of /SELECT/ are as follows.
The predicates /predi/ are evaluated in some arbitrary
order, or possibly even in parallel.
If none of
them is /TRUE/, then the value of /default\value/
is the value of the /SELECT/. Otherwise, one of
the values corresponding to a /TRUE/ predicate is
chosen in some arbitrary fashion and evaluated to
produce the value of
the /SELECT/.⊗⊗The order, if any, in which
the predicates are evaluated, and the
manner in which
the value is chosen if more than
one predicate is true, are
purposely undefined. It could be done
by using some arbitrary ordering chosen by the compiler, or
by using a pseudo-random number generator at run time, or by
any other method.
Naturally, if exactly one predicate
is /TRUE/, then the corresponding value $must$
be chosen as the value of the /SELECT/ statement.
One perfectly valid way to compile it would be to treat it
as if it were written like a LISP /COND/ statement,
for example.
On the other hand, it is $not$ valid for the user
of a /SELECT/ statement to assume that it will
be compiled in this way.⊗
Exactly one of the /valuei/ and /default\value/
is evaluated at all, and that will be the one chosen
to supply the value of the /SELECT/ statement.
As a matter of convenience, we will allow two conventions
on defaulting. If the /default\value/ is /NOTHING/,
then we may write /END/ instead of /ELSE NOTHING/.
Also, if any predicate is $identically$ /TRUE/, then we
may omit the /[TRUE]/ and merely write the corresponding value.
Using the /SELECT/ statement, we can easily translate a
simple /EITHER/ construct. For example, the construct:
.beginecl
EITHER this\action
OR that\action
OR other\action
END\OR
.endecl
would translate directly into:
.beginecl
↑↑↑↑SELECT
↑↑↑↑↑translation\of\this\action;
↑↑↑↑↑translation\of\that\action;
↑↑↑↑↑translation\of\other\action;
↑↑↑↑END
.endecl
which is in fact an abbreviation for:
.beginecl
↑↑↑↑SELECT
↑↑↑↑↑[TRUE] translation\of\this\action;
↑↑↑↑↑[TRUE] translation\of\that\action;
↑↑↑↑↑[TRUE] translation\of\other\action;
↑↑↑↑ELSE NOTHING
.endecl
If the /EITHER/ construct is embedded within a /TRY/
construct, then the predicates of the /SELECT/ statement
are necessary. Thus the construct:
.beginecl
TRY EITHER IF STARTUP(WRITER) POSSIBLE
OR IF STARTUP(ALL READER) POSSIBLE
END\OR
END\TRY
.endecl
would translate into this /SELECT/ statement:
.beginecl
↑↑↑↑SELECT
↑↑↑↑↑[WRITER\COUNT GT 0]
↑↑↑↑↑↑[) WRITER\COUNT ∀← WRITER\COUNT - 1;
↑↑↑↑↑↑ εVε(WRITER\SEM) (];
↑↑↑↑↑[READER\COUNT GT 0]
↑↑↑↑↑↑REPEAT
↑↑↑↑↑↑↑READER\COUNT = 0 => NOTHING;
↑↑↑↑↑↑↑READER\COUNT ∀← READER\COUNT - 1;
↑↑↑↑↑↑↑εVε(READER\SEM);
↑↑↑↑↑↑END;
↑↑↑↑END
.endecl
As a more complicated example, indicating the use
of the /ELSE/ clause of the /SELECT/ statement, consider
this two-level /TRY/ construct:
.beginecl
TRY EITHER IF STARTUP(PROC1A) POSSIBLE
OR IF STARTUP(PROC1B) POSSIBLE
END\OR
NEXT EITHER IF STARTUP(PROC2A) POSSIBLE
OR IF STARTUP(PROC2B) POSSIBLE
END\OR
END\TRY
.endecl
Recall that the semantics of this are that a /PROC1A/
or a /PROC1B/ is started up if either one is possible,
but the choice of which is arbitrary if both are possible;
if neither are possible (neither waitset contains any processes),
then a similar choice is made between the waitsets
/PROC2A/ and /PROC2B/. The translation of this is as follows:
.beginecl
↑↑↑↑SELECT
↑↑↑↑↑[PROC1A\COUNT GT 0]
↑↑↑↑↑↑↑[) PROC1A\COUNT ∀← PROC1A\COUNT - 1;
↑↑↑↑↑↑↑ εVε(PROC1A\SEM) (];
↑↑↑↑↑[PROC1B\COUNT GT 0]
↑↑↑↑↑↑↑[) PROC1B\COUNT ∀← PROC1B\COUNT - 1;
↑↑↑↑↑↑↑ εVε(PROC1B\SEM) (];
↑↑↑↑ELSE SELECT
↑↑↑↑↑[PROC2A\COUNT GT 0]
↑↑↑↑↑↑↑[) PROC2A\COUNT ∀← PROC2A\COUNT - 1;
↑↑↑↑↑↑↑ εVε(PROC2A\SEM) (];
↑↑↑↑↑[PROC2B\COUNT GT 0]
↑↑↑↑↑↑↑[) PROC2B\COUNT ∀← PROC2B\COUNT - 1;
↑↑↑↑↑↑↑ εVε(PROC2B\SEM) (];
↑↑↑↑END
.endecl
This fairly complicated example demonstrates the flexibility
of /SELECT/. One great advantage of /SELECT/ is that it requires
no failure backup in the way the /EITHER/, at least on the surface,
would seem to require. Another advantage is that it lends itself
well to certain kinds of code motion and code merging
(see chapter @chapoptimize@).
.section bruteexample,Example of Brute Force Translation
As an example of the application of the translation
methods described in this chapter, let us consider the
$Simple Mutual Exclusion Problem$.⊗⊗This example is
identical to that used in section @exclusion@.⊗
In this problem there are a number of identical processes
which all wish occasionally to access a data base;
no more than one process may access the data base at a time,
however.
The SAL assertions for this problem are as follows:
.beginecl
<↑UNLOCKED IS LOCK = 0,
↑LOCKED IS LOCK = 1,
↑SOMEBODY DOES
↑↑BEGIN
↑↑↑ASSERT(UNLOCKED, LOCKED);
↑↑↑CIA("LOCK\DATA\BASE");
↑↑↑ASSERT(UNLOCKED ==> LOCKED, ELSE WAIT);
↑↑↑IE "HACK DATA BASE";
↑↑↑ASSERT(LOCKED);
↑↑↑CIA("UNLOCK\DATA\BASE");
↑↑↑ASSERT(ALWAYS UNLOCKED THEN TRY
↑↑↑↑↑IF REVIVE(SOMEBODY) POSSIBLE
↑↑↑↑END\TRY);
↑↑END >
.endecl
The code produced by the SAL synthesizer for the
two synchronization functions are as follows:
.beginecl
↑LOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑LOCK = FALSE => LOCK ∀← NOT LOCK;
↑↑↑↑ENTERL(LASTRUN, SOMEBODY);
↑↑↑↑LASTRUN ∀← NIL;
↑↑↑END;
.endecl
.beginecl
↑UNLOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑SOMEBODY α# NIL =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑LASTRUN α# NIL -> ENTERL(LASTRUN, INACTIVEQ);
↑↑↑↑↑↑LASTRUN ∀← REMOVEF(SOMEBODY);
↑↑↑↑↑↑LOCK\DATA\BASE();
↑↑↑↑↑END;
↑↑↑END;
.endecl
Note the means by which the SAL synthesizer translates
the /REVIVE/ actions into CI primitives: it causes
the current process to be put on /INACTIVEQ/,
removes the other process from the waitset and puts it
in /LASTRUN/ so that it will be the next process
to be run, and then invokes the
synchronization function of the revived process as
an actual EL1 subroutine. For a semaphore implementation
this is not practical, as will be seen.
In order to convert these functions to use semaphore
primitives, we retain the state variables manipulations
created by the synthesizer, but re-translate the SAL
actions, and add in the generated tag and
the auxiliary operations on
the semaphore /mutex/. This results in the following code:
.beginecl
↑LOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑TAG1:
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK = FALSE =>
↑↑↑↑↑↑[) LOCK ∀← NOT LOCK;
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑SOMEBODY\COUNT ∀← SOMEBODY\COUNT + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(SOMEBODY\SEM);
↑↑↑↑GOTO TAG1;
↑↑↑END;
.endecl
.beginecl
↑UNLOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑TAG2:
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑SOMEBODY\COUNT GT 0 =>
↑↑↑↑↑↑[) SOMEBODY\COUNT ∀← SOMEBODY\COUNT - 1;
↑↑↑↑↑↑ εVε(SOMEBODY\SEM);
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
Note, in /LOCK\DATA\BASE/, that the /WAIT/ action was translated
as a εPε-operation followed by a /GOTO/ to the tag at the top
of the function, and that the ↓_εVε_↓/(mutex)/ was placed $between$
the incrementation of the count and the εPε-operation.
It may be argued that this precise sequence is necessary
if timing errors are to be avoided: the incrementation must
be done before the εVε/(mutex)/ or else some other process might
see the wrong value for the counter and fail to perform a
/STARTUP/ on a process which was actually waiting (or rather, "about
to wait"); on the other hand, the ↓_εVε_↓/(mutex)/ must certainly be performed
before the εPε-operation, which might potentially block the
executing process.
Note too, what occurs when a /REVIVE/ is performed:
a εVε-operation occurs on /SOMEBODY\SEM/, allowing some other
process to execute the /GOTO/ to the top of the /LOCK\DATA\BASE/
synchronization function for that process and so repeat that
function, as specified by the /REVIVE/ action.
.chapter chapmutex,The Subtle Mutual Exclusion Problem
As mentioned at the beginning of chapter @chapbrute@,
the brute force translation techniques carry within them a
subtle timing problem which renders the generated code
incorrect. It will be instructive to consider this problem
very carefully, for it is typical of the kind of problem
which tends to haunt any code written in terms of semaphore
primitives. We will find that it will be possible to correct
the problem, but only with some change in our translation
strategy.
.section mutexproblem,The Problem
The problem with the brute force methods of translation
is that the translation of /REVIVE/ is not quite correct.
As mentioned in section @actionrevive@,
"the result assertion of the revived process takes effect before
any other process gets into the CI"; this is part of the very
definition of the /REVIVE/ action in SAL.
Unfortunately, our brute force translation of /REVIVE/
fails to preserve this important property.
In order to see this, let us consider such a failure to
"pass the mutual exclusion" in a particular system of processes:
.beginecl
<↑LOCKED IS LOCK = TRUE,
↑UNLOCKED IS LOCK = FALSE,
↑HIGH\PRIORITY\PROCESS DOES
↑↑BEGIN
↑↑ASSERT(LOCKED, UNLOCKED);
↑↑CIA("HIGH\PRIORITY\WAIT");
↑↑ASSERT(UNLOCKED ==> LOCKED, ELSE WAIT);
↑↑IE "HACK DATA BASE";
↑↑ASSERT(LOCKED);
↑↑CIA("HIGH\PRIORITY\RELEASE");
↑↑ASSERT(ALWAYS UNLOCKED THEN
↑↑↑↑TRY IF REVIVE(HIGH\PRIORITY\PROCESS) POSSIBLE
↑↑↑↑NEXT IF REVIVE(LOW\PRIORITY\PROCESS) POSSIBLE
↑↑↑↑END\TRY);
↑↑END,
↑LOW\PRIORITY\PROCESS DOES
↑↑BEGIN
↑↑ASSERT(LOCKED, UNLOCKED);
↑↑CIA("LOW\PRIORITY\WAIT");
↑↑ASSERT(UNLOCKED ==> LOCKED, ELSE WAIT);
↑↑IE "HACK DATA BASE";
↑↑ASSERT(LOCKED);
↑↑CIA("LOW\PRIORITY\RELEASE");
↑↑ASSERT(ALWAYS UNLOCKED THEN
↑↑↑↑TRY IF REVIVE(HIGH\PRIORITY\PROCESS) POSSIBLE
↑↑↑↑NEXT IF REVIVE(LOW\PRIORITY\PROCESS) POSSIBLE
↑↑↑↑END\TRY);
↑↑END >
.endecl
This system is similar to that considered in section @bruteexample@,
but has two kinds of processes. No more than one process
may have access to the data base at a time; furthermore,
any waiting processes of the first kind have priority over those
of the second kind.
Let us consider in particular a possible
sequence of events for three distinguished
processes /A/, /B/, and /C/ (and assume no interference on the part
of any other processes in the system).
Let /B/ be a high-priority process, and let /C/ be a low-priority
process. Suppose, then, that initially process /A/ has access to
the data base. Process /B/ executes its first /CIA/ call,
finds that the data base is locked, and so performs the /WAIT/ action.
Process /A/ completes its data base access, and executes its second
/CIA/ call; in doing so it finds that it is possible to revive a
high-priority process, namely /B/. At this point process /C/
attempts to execute its first /CIA/ call. It finds that it cannot,
because process /A/ has possession of the CI. Furthermore, it will not
be able to until the actions of process /B/'s first synchronization
function have taken effect (by the definition of the
/REVIVE/ action) and process /B/ is permitted to proceed.
This is all as it should be: process /B/, having higher priority,
gets in before process /C/.
Now we shall examine the semaphore code produced
by brute force translation of the synchronization functions
for the processes.
The code produced by the SAL synthesizer for the four
synchronization functions is as follows:
.beginecl
↑HIGH\PRIORITY\WAIT ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑LOCK = FALSE => LOCK ∀← NOT LOCK;
↑↑↑↑ENTERL(LASTRUN, HIGH\PRIORITY\PROCESS);
↑↑↑↑LASTRUN ∀← NIL;
↑↑↑END;
.endecl
.beginecl
↑HIGH\PRIORITY\RELEASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑HIGH\PRIORITY\PROCESS α# NIL =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑LASTRUN α# NIL -> ENTERL(LASTRUN, INACTIVEQ);
↑↑↑↑↑↑LASTRUN ∀← REMOVEF(HIGH\PRIORITY\PROCESS);
↑↑↑↑↑↑HIGH\PRIORITY\WAIT();
↑↑↑↑↑END;
↑↑↑↑LOW\PRIORITY\PROCESS α# NIL =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑LASTRUN α# NIL -> ENTERL(LASTRUN, INACTIVEQ);
↑↑↑↑↑↑LASTRUN ∀← REMOVEF(LOW\PRIORITY\PROCESS);
↑↑↑↑↑↑LOW\PRIORITY\WAIT();
↑↑↑↑↑END;
↑↑↑END;
.endecl
.beginecl
↑LOW\PRIORITY\WAIT ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑LOCK = FALSE => LOCK ∀← NOT LOCK;
↑↑↑↑ENTERL(LASTRUN, LOW\PRIORITY\PROCESS);
↑↑↑↑LASTRUN ∀← NIL;
↑↑↑END;
.endecl
.beginecl
↑LOW\PRIORITY\RELEASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑HIGH\PRIORITY\PROCESS α# NIL =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑LASTRUN α# NIL -> ENTERL(LASTRUN, INACTIVEQ);
↑↑↑↑↑↑LASTRUN ∀← REMOVEF(HIGH\PRIORITY\PROCESS);
↑↑↑↑↑↑HIGH\PRIORITY\WAIT();
↑↑↑↑↑END;
↑↑↑↑LOW\PRIORITY\PROCESS α# NIL =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑LASTRUN α# NIL -> ENTERL(LASTRUN, INACTIVEQ);
↑↑↑↑↑↑LASTRUN ∀← REMOVEF(LOW\PRIORITY\PROCESS);
↑↑↑↑↑↑LOW\PRIORITY\WAIT();
↑↑↑↑↑END;
↑↑↑END;
.endecl
Now, following the rules laid out in chapter @chapbrute@,
we translate this code into code using semaphores:
.beginecl
↑HIGH\PRIORITY\WAIT ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑TAG1:
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK = FALSE =>
↑↑↑↑↑↑[) LOCK ∀← NOT LOCK;
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(HIGH\PRIORITY\PROCESS\SEM);
↑↑↑↑GOTO TAG1;
↑↑↑END;
.endecl
.beginecl
↑HIGH\PRIORITY\RELEASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑TAG2:
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT GT 0 =>
↑↑↑↑↑↑[) HIGH\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT - 1;
↑↑↑↑↑↑ εVε(HIGH\PRIORITY\PROCESS\SEM);
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑LOW\PRIORITY\PROCESS\COUNT GT 0 =>
↑↑↑↑↑↑[) LOW\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑↑↑LOW\PRIORITY\PROCESS\COUNT - 1;
↑↑↑↑↑↑ εVε(LOW\PRIORITY\PROCESS\SEM);
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
.beginecl
↑LOW\PRIORITY\WAIT ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑TAG3:
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK = FALSE =>
↑↑↑↑↑↑[) LOCK ∀← NOT LOCK;
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑LOW\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑LOW\PRIORITY\PROCESS\COUNT + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(LOW\PRIORITY\PROCESS\SEM);
↑↑↑↑GOTO TAG3;
↑↑↑END;
.endecl
.beginecl
↑LOW\PRIORITY\RELEASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑TAG4:
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT GT 0 =>
↑↑↑↑↑↑[) HIGH\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT - 1;
↑↑↑↑↑↑ εVε(HIGH\PRIORITY\PROCESS\SEM);
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑LOW\PRIORITY\PROCESS\COUNT GT 0 =>
↑↑↑↑↑↑[) LOW\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑↑↑LOW\PRIORITY\PROCESS\COUNT - 1;
↑↑↑↑↑↑ εVε(LOW\PRIORITY\PROCESS\SEM);
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
Now let us consider the three processes /A/, /B/, and /C/
using this brute-force-generated semaphore code.
Suppose, as before, that initially process /A/ has access to
the data base. Process /B/ executes its first synchronization
function (/HIGH\PRIORITY\WAIT/), discovers that the state variable
/LOCK/ is /TRUE/, and so increments /HIGH\PRIORITY\PROCESS\COUNT/,
unlocks the mutual exclusion semaphore /mutex/, and attempts to perform
↓_εPε_↓/(HIGH\PRIORITY\PROCESS\SEM)/, but is blocked.
Process /A/ completes its data base access, and executes its second
synchronization function;
in doing so it finds that it is possible to revive a
high-priority process, namely /B/, because /HIGH\PRIORITY\PROCESS\COUNT/
is greater than zero. Process /A/ therefore performs
↓_εVε_↓/(HIGH\PRIORITY\PROCESS\SEM)/, and process /B/ succeeds in
performing ↓_εPε_↓/(HIGH\PRIORITY\PROCESS\SEM)/, and then goes
on to perform /GOTO#TAG1/. Process /A/ then performs ↓_εVε_↓/(mutex)/.
At this point process /C/, our villain,
executes its first synchronization function (/LOW\PRIORITY\WAIT/).
Now process /B/, being a very slow process, let us assume, has not
finished executing /GOTO#TAG1/; it therefore has not yet executed
the ↓_εPε_↓/(mutex)/ following /TAG1/.
Process /C/, being a very fast process, let us assume,
therefore $succeeds$ in performing ↓_εPε_↓/(mutex)/.
Process /C/ then finds that the state variable /LOCK/
is /FALSE/, and so sets it to /TRUE/ and gains access to the data base.
We find, then, that our semaphore code is $not$
an accurate translation of the original SAL specifications,
for it allows low-priority processes to get in ahead of revived
high-priority processes. More generally, it does not preserve the
"immediate execution" property of the SAL /REVIVE/ action, and
so any system programmed in SAL which depends on this property of
/REVIVE/ will not be correctly translated into semaphore code
by the brute-force methods of chapter @chapbrute@.
.section mutexsolutions,Possible Solutions
There are a number of ways in which we may resolve the
problem of the translation of /REVIVE/, each imposing a radical
change of one kind or another on the translation system
composed of the SAL synthesizer and semaphore code generator.
One of these in particular will not only solve the problem,
but also open the door to a whole new realm of consideration,
i.e. optimization of the generated semaphore code;
this will be the subject of chapters @chapoptimize@
and @chapexamples@.
.subsec solnloser,|Caveat Emptor; or, Let the Loser Lose|
One method of "solving" the problem is to borrow
a technique from modern-day empirical programming style;
that is, to declare the "bug" to be a "feature".
We might redefine the SAL /REVIVE/ action $not$ to "pass
the mutual exclusion" of the CI from process to process,
but allow slip-through of the kind already considered
in section @mutexproblem@.
Don't laugh, now! For certain kinds of applications
this might actually be an acceptable solution. After all,
if the passing of mutual exclusion is not critical for
a given application, then the brute-force translation
will produce perfectly acceptable code. On the other
hand, there are probably some applications (including
the priority level problem we have just considered)
which seem to require this exclusion in order to function
at all. In fact, the "immediate execution" property
of the /REVIVE/ action is largely what gives SAL its
expressive power. We must conclude, then, that "caveat
emptor" is not an acceptable solution to our problem.
.subsec solnsplit,State Splitting
Another approach we might take is to split the states
of the system by introducing extra variables.
Thus, in the example above, we might split the state /UNLOCKED/
into three states, namely /UNLOCKED/, /UNLOCKED\FOR\HIGH\PRIORITY\PROCESS/,
and /UNLOCKED\FOR\LOW\PRIORITY\PROCESS/.
More generally, for any result assertion of the form:
.beginecl
↑↑OLD\STATE ==> NEW\STATE THEN REVIVE(PROCESS OUTOF RANDOM\QUEUE)
.endecl
it would be necessary to create an extra state called
/NEW\STATE\FOR\RANDOM\QUEUE/. Such a state would mean
that only processes newly revived from /RANDOM\QUEUE/ would be permitted
to consider the system as being in /NEW\STATE/ for purposes
of their synchronization functions.
Suppose that we create a new variable and effectively define new
states as follows:
.beginecl
<↑LOCKED IS LOCK = TRUE,
↑UNLOCKED IS LOCK = FALSE AND PRIORITY\SWITCH = 0,
↑UNLOCKED\FOR\HIGH\PRIORITY\PROCESS IS
↑↑↑LOCK = FALSE AND PRIORITY\SWITCH = 1,
↑UNLOCKED\FOR\LOW\PRIORITY\PROCESS IS
↑↑↑LOCK = FALSE AND PRIORITY\SWITCH = 2,
↑...
.endecl
Then a solution to the priority problem of section @mutexproblem@
using state splitting might look like this:
.beginecl
↑HIGH\PRIORITY\WAIT ←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑TAG1:
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK = FALSE AND
↑↑↑↑↑↑↑(PRIORITY\SWITCH = 0 OR
↑↑↑↑↑↑↑↑PRIORITY\SWITCH = 1) =>
↑↑↑↑↑↑[) LOCK ∀← NOT LOCK;
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(HIGH\PRIORITY\PROCESS\SEM);
↑↑↑↑GOTO TAG1;
↑↑↑END;
.endecl
.beginecl
↑HIGH\PRIORITY\RELEASE ←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑TAG2:
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT GT 0 =>
↑↑↑↑↑↑[) HIGH\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT - 1;
↑↑↑↑↑↑ PRIORITY\SWITCH ∀← 1;
↑↑↑↑↑↑ εVε(HIGH\PRIORITY\PROCESS\SEM);
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑LOW\PRIORITY\PROCESS\COUNT GT 0 =>
↑↑↑↑↑↑[) LOW\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑↑↑LOW\PRIORITY\PROCESS\COUNT - 1;
↑↑↑↑↑↑ PRIORITY\SWITCH ∀← 2;
↑↑↑↑↑↑ εVε(LOW\PRIORITY\PROCESS\SEM);
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑PRIORITY\SWITCH ∀← 0;
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
.beginecl
↑LOW\PRIORITY\WAIT ←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑TAG3:
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK = FALSE AND
↑↑↑↑↑↑↑(PRIORITY\SWITCH = 0 OR
↑↑↑↑↑↑↑↑PRIORITY\SWITCH = 2) =>
↑↑↑↑↑↑[) LOCK ∀← NOT LOCK;
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑LOW\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑LOW\PRIORITY\PROCESS\COUNT + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(LOW\PRIORITY\PROCESS\SEM);
↑↑↑↑GOTO TAG3;
↑↑↑END;
.endecl
.beginecl
↑LOW\PRIORITY\RELEASE ←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑TAG4:
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT GT 0 =>
↑↑↑↑↑↑[) HIGH\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT - 1;
↑↑↑↑↑↑ PRIORITY\SWITCH ∀← 1;
↑↑↑↑↑↑ εVε(HIGH\PRIORITY\PROCESS\SEM);
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑LOW\PRIORITY\PROCESS\COUNT GT 0 =>
↑↑↑↑↑↑[) LOW\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑↑↑LOW\PRIORITY\PROCESS\COUNT - 1;
↑↑↑↑↑↑ PRIORITY\SWITCH ∀← 2;
↑↑↑↑↑↑ εVε(LOW\PRIORITY\PROCESS\SEM);
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑PRIORITY\SWITCH ∀← 0;
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
Unfortunately, it is not clear how general this technique is.
It seems to require the existence of an /ELSE/ clause
in every result assertion which also contains (possibly in another
result transition) a /WAIT/ action from which the process
will be revived. This is necessary so that it will be clear what to
do if the system is in a generated state.⊗⊗It is not an accident
that the example of section @mutexproblem@ which we have been considering
has precisely this property!⊗
This may not be a great restriction, but it limits the generality
of the solution.
The state-splitting approach also suffers from state
explosion; that is, for large systems a very large number of new
states and variables may have to be generated, as well as
code to maintain and test for these states and variables.
Because of these limitations, the state-splitting approach, while
not necessarily infeasible, will not be considered further in this
thesis.
.subsec solnurgent,The /urgentcount/ Approach
Hoare [{hoare}] has a problem in translating monitors
to semaphores similar to that plaguing us here;
that is, monitors wish to "pass the mutual exclusion"
in a manner similar to that of /REVIVE/.
We might consider, then, adopting Hoare's /urgentcount/
strategy. Briefly, this strategy entails introducing an
extra integer variable /urgentcount/ and an extra semaphore
/urgent/. Furthermore some changes are introduced into
the generated semaphore code. First of all,
in any synchronization function which contains code
for a revivable /WAIT/ action exits,
each occurrence of:
.beginecl
↑εVε(mutex);
.endecl
must be replaced by:
.beginecl
↑[) urgentcount GT 0 => εVε(urgent); εVε(mutex) (];
.endecl
Also, in translating the /REVIVE/ action,
we must replace the operation:
.beginecl
↑εVε(FOO\SEM);
.endecl
with the code:
.beginecl
↑[) urgentcount ∀← urgentcount + 1;
↑ εVε(FOO\SEM);
↑ εPε(urgent);
↑ urgentcount ∀← urgentcount - 1 (];
.endecl
Finally, in each synchronization function we
will exchange the positions of the generated tag
and the ↓_εPε_↓/(mutex)/, so that the latter comes first.
Using this approach a solution to the problem of section
@mutexproblem@ would look like this:
.beginecl
↑HIGH\PRIORITY\WAIT ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑TAG1:
↑↑↑↑LOCK = FALSE =>
↑↑↑↑↑↑[) LOCK ∀← NOT LOCK;
↑↑↑↑↑↑ [) urgentcount GT 0 => εVε(urgent);
↑↑↑↑↑↑ εVε(mutex) (]; (];
↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT + 1;
↑↑↑↑[) urgentcount GT 0 => εVε(urgent);
↑↑↑↑ εVε(mutex) (];
↑↑↑↑εPε(HIGH\PRIORITY\PROCESS\SEM);
↑↑↑↑GOTO TAG1;
↑↑↑END;
.endecl
.beginecl
↑HIGH\PRIORITY\RELEASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑TAG2:
↑↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT GT 0 =>
↑↑↑↑↑↑[) HIGH\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT - 1;
↑↑↑↑↑↑ urgentcount ∀← urgentcount + 1;
↑↑↑↑↑↑ εVε(HIGH\PRIORITY\PROCESS\SEM);
↑↑↑↑↑↑ εPε(urgent);
↑↑↑↑↑↑ urgentcount ∀← urgentcount - 1;
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑LOW\PRIORITY\PROCESS\COUNT GT 0 =>
↑↑↑↑↑↑[) LOW\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑↑↑LOW\PRIORITY\PROCESS\COUNT - 1;
↑↑↑↑↑↑ urgentcount ∀← urgentcount + 1;
↑↑↑↑↑↑ εVε(LOW\PRIORITY\PROCESS\SEM);
↑↑↑↑↑↑ εPε(urgent);
↑↑↑↑↑↑ urgentcount ∀← urgentcount - 1;
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
.beginecl
↑LOW\PRIORITY\WAIT ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑TAG3:
↑↑↑↑LOCK = FALSE =>
↑↑↑↑↑↑[) LOCK ∀← NOT LOCK;
↑↑↑↑↑↑ [) urgentcount GT 0 => εVε(urgent);
↑↑↑↑↑↑ εVε(mutex) (]; (];
↑↑↑↑LOW\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑LOW\PRIORITY\PROCESS\COUNT + 1;
↑↑↑↑[) urgentcount GT 0 => εVε(urgent);
↑↑↑↑ εVε(mutex) (];
↑↑↑↑εPε(LOW\PRIORITY\PROCESS\SEM);
↑↑↑↑GOTO TAG3;
↑↑↑END;
.endecl
.beginecl
↑LOW\PRIORITY\RELEASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑TAG4:
↑↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT GT 0 =>
↑↑↑↑↑↑[) HIGH\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT - 1;
↑↑↑↑↑↑ urgentcount ∀← urgentcount + 1;
↑↑↑↑↑↑ εVε(HIGH\PRIORITY\PROCESS\SEM);
↑↑↑↑↑↑ εPε(urgent);
↑↑↑↑↑↑ urgentcount ∀← urgentcount - 1;
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑LOW\PRIORITY\PROCESS\COUNT GT 0 =>
↑↑↑↑↑↑[) LOW\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑↑↑LOW\PRIORITY\PROCESS\COUNT - 1;
↑↑↑↑↑↑ urgentcount ∀← urgentcount + 1;
↑↑↑↑↑↑ εVε(LOW\PRIORITY\PROCESS\SEM);
↑↑↑↑↑↑ εPε(urgent);
↑↑↑↑↑↑ urgentcount ∀← urgentcount - 1;
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
Now let us consider the three processes /A/, /B/, and /C/
using the /urgentcount/ solution.
Suppose, as before, that initially process /A/ has access to
the data base. Process /B/ executes its first synchronization
function (/HIGH\PRIORITY\WAIT/), discovers that the state variable
/LOCK/ is /TRUE/, and so increments /HIGH\PRIORITY\PROCESS\COUNT/.
Since at this point /urgentcount/ is zero (its normal value),
process /B/
unlocks the mutual exclusion semaphore /mutex/, and attempts to perform
↓_εPε_↓/(HIGH\PRIORITY\PROCESS\SEM)/, but is blocked.
Process /A/ completes its data base access, and executes its second
synchronization function;
in doing so it finds that it is possible to revive a
high-priority process, namely /B/, because /HIGH\PRIORITY\PROCESS\COUNT/
is greater than zero. Process /A/ therefore increments
/urgentcount/ and then performs
↓_εVε_↓/(HIGH\PRIORITY\PROCESS\SEM)/, and process /B/ succeeds in
performing ↓_εPε_↓/(HIGH\PRIORITY\PROCESS\SEM)/, and then goes
on to perform /GOTO#TAG1/. Process /A/ then performs ↓_εPε_↓/(urgent)/.
At this point process /C/ attempts to execute its first
synchronization function (/LOW\PRIORITY\WAIT/), but is blocked,
because process /A/ never performed ↓_εVε_↓/(mutex)/.
Now process /B/ will eventually perform /GOTO#TAG1/,
discover that /LOCK/ is /FALSE/, and so will perform
/LOCK#/↓_∀←_↓/#NOT#LOCK/ and exit.
In exiting, it sees that /urgentcount/ is positive,
and so does not perform ↓_εVε_↓/(mutex)/, but rather
↓_εVε_↓/(urgent)/. This will allow process /A/ to proceed.
Note that during all of this process /C/ has been blocked,
and will remain blocked until process /A/ finishes
its synchronization function.
.next page << losing footnote >>
This is indeed a clever and elegant solution.
Unfortunately there is one major problem with it;
this problem occurs when /REVIVE/ operations are $nested$,
i.e. process /X/ revives process /Y/, which in turn
revives process /Z/. When process /Z/'s synchronization
function is running, the value of /urgentcount/ is 2,
and both /X/ and /Y/ are waiting on the semaphore /urgent/.
When process /Z/ eventually performs ↓_εVε_↓/(urgent)/,
it is indeterminate which of /X/ and /Y/ will be allowed
to proceed.
Thus, when the /REVIVE/ actions are nested,
the /urgentcount/ approach does not correctly impose
a strict subroutine calling discipline.
This will not hurt in some cases
(e.g. the case where no synchronization
function ever does anything but exit after reviving
another process), but in general will not produce
correct results. Therefore we will reject the
/urgentcount/ approach also.⊗⊗It is worth
noting, as Hoare does, that /urgentcount/
is not needed at all, even for nested
/REVIVE/ operations, if each reviving
process does only one /REVIVE/, if any,
and that just prior to exiting the synchronization
function. This may be important in practice,
since problems which do not use /REVIVE(ALL#...)/
may well conform to this restriction.⊗
.subsec solnextract,Code Extraction
One more approach we could try is
that of $code extraction$. Rather than trying
to coerce the revived process into re-executing
its synchronization function, we may extract the
relevant code at translation time from the function
for the revived process and put that code into
the function for the reviving process.
To put it another way, we may recall that
the advantage of /REVIVE/ over /STARTUP/
is that the former does not require the reviving function to
have any knowledge of the state transformations
desired by the revived function; turning this around,
we may convert a difficult-to-translate
/REVIVE/ into an easy-to-translate
/STARTUP/ by fetching this knowledge
mechanically and putting it in the reviving
function when it is translated.
There is one problem with this approach,
however, which needs to be faced at once: it is not
immediately clear what to do with extracted
code which contains a /WAIT/ action.
A little thought will show, however, that this is not
insurmountable; the solution to this obstacle will
be discussed in chapter @chapbug@.
Another problem may arise in connection
with occurrences of /IF#REVIVE(...)#POSSIBLE/
which nest in a circular manner (i.e. they are statically
circular, although not dynamically, since the
/IF#...#POSSIBLE/ construct provides a
conditional termination for the circularity).
Such circularities cause indefinite extraction loops
to occur. It may be possible to recognize such loops
and actually compile them as loops of some kind
rather than attempting to endlessly extract code.
No practical synchronization problems
seem to require such circularities, and so this problem
is not investigated further in this thesis.
Since the code extraction method therefore
seems to handle (almost) all cases without the difficulties
of the other techniques, we will proceed to
explore the code extraction method more fully
in the remainder of this thesis.
.chapter chapextract,Translation with Code Extraction
This chapter is similar in structure to
chapter @chapbrute@; we will, however, be considering
the code extraction translation method suggested in
section @solnextract@ rather than
the previous "brute-force" method.
The reader may find it helpful to correlate the various
sections of this chapter with those of
chapter @chapbrute@.
.section extractstrategy,General Translation Strategy
As in chapter @chapbrute@ we will use
semaphores to represent waitsets, possibly with
associated counters used to keep track of the number of
processes in each waitset; we will also use the
semaphore /mutex/ to enforce mutual exclusion.
The primary difference
will occur in the translation of /WAIT/
and /REVIVE/. Note that since we will,
in effect, be turning each /REVIVE/
into a /STARTUP/ preceded by code to
effect the result assertions for the revived
process, in principle we may lift our previously
imposed restriction about mixing /STARTUP/
and /REVIVE/ on a single waitset (though,
as mentioned before, in practice such mixing
seems not to be particularly useful).
Also, because no /GOTO/ will be needed to
translate /WAIT/, no tag need be generated
at the beginning of each synchronization function.
.section extracttrans,Translation of SAL Primitives
Most of the SAL primitives will be
translated in much the same way they were in chapter
@chapbrute@, but for completeness and accuracy
the translation methods using code extraction
will be described here for all SAL primitives.
.subsec etranswait,Translation of /WAIT/
We will not ever need to translate the
/WAIT/ action using a /GOTO/,
but we still may need an associated counter.
Hence there will be two ways to translate
the action:
.beginecl
WAIT IN FOO
.endecl
They differ only in whether the counter must
be incremented:
.skip continue
(1) Without counter:
.beginecl
↑↑↑↑εPε(FOO\SEM)
.endecl
(2) With counter:
.beginecl
↑↑↑↑[) FOO\COUNT ∀← FOO\COUNT - 1;
↑↑↑↑ εPε(FOO\SEM) (]
.endecl
.subsec etransstartup,Translation of /STARTUP/
Translation of /STARTUP/ will be
precisely as described in section @primstartup@.
That is, for the SAL action:
.beginecl
STARTUP(PROCESS OUTOF FOO)
.endecl
there are two translations, as for /WAIT/:
.skip continue
(1) Without counter:
.beginecl
↑↑↑↑εVε(FOO\SEM)
.endecl
(2) With counter:
.beginecl
↑↑↑↑[) FOO\COUNT ∀← FOO\COUNT - 1;
↑↑↑↑ εVε(FOO\SEM) (]
.endecl
.subsec etransrevive,Translation of /REVIVE/
In order to translate the /REVIVE/
action, code extraction is needed.
Suppose that the action to be translated is:
.beginecl
REVIVE(PROCESS OUTOF FOO)
.endecl
Then we shall translate this as follows, if a counter
is needed:⊗⊗There is a problem with this that
will be dealt with in chapter @chapbug@.⊗
.beginecl
↑↑↑↑[) FOO\COUNT ∀← FOO\COUNT - 1;
↑↑↑↑ extracted\result\assertion\code;
↑↑↑↑ εVε(FOO\SEM) (]
.endecl
.next page << fix footnote loss >>
The extracted code is, in effect, the entire
synchronization function for the revived process
with all code involving /mutex/ removed.⊗⊗This
may strike the reader as fairly clumsy, since we should
really need only the code which deals with the state
we have just put the system into. In fact, in examples
we will find it convenient to immediately perform
the optimization of realizing which state the system is
in and extracting only the relevant code; in fact, this
is necessary to the translation of
/REVIVE(ALL#...)/, as will be seen in
section @etransreviveall@. This whole issue
will be dealt with more generally in chapter
@chapoptimize@, however.⊗
As a very informal example, consider these
two result assertions for two different processes:
.beginecl
↑ASSERT(UNLOCKED ==> LOCKED, ELSE WAIT);
↑ASSERT(ALWAYS UNLOCKED THEN
↑↑↑TRY IF REVIVE(SOMEBODY) POSSIBLE END\TRY);
.endecl
(These are in fact the result assertions for the
$Simple Mutual Exclusion Problem$ considered
in section @bruteexample@.)
We would effectively translate these as if they
were written something like this (which is written
here, to get the idea across,
as a mixture of EL1 code and SAL
assertions, which of course may not be mixed in practice!):
.beginecl
↑ASSERT(UNLOCKED ==> LOCKED, ELSE WAIT);
↑ASSERT(ALWAYS UNLOCKED THEN
↑↑↑STARTUP\POSSIBLE(SOMEBODY) =>
↑↑↑↑↑[) SOMEBODY\COUNT ∀← SOMEBODY\COUNT - 1;
↑↑↑↑↑ [) UNLOCKED ==> LOCKED, ELSE WAIT (];
↑↑↑↑↑ STARTUP(SOMEBODY) (]);
.endecl
.subsec etransstartupall,|Translation of /STARTUP(ALL ...)/|
The /STARTUP(ALL#...)/ action
will be translated just as described in section
@primall@; that is, the action:
.beginecl
STARTUP(ALL PROCESS OUTOF FOO)
.endecl
is translated into the following "canned" loop:
.beginecl
↑↑↑↑REPEAT
↑↑↑↑↑FOO\COUNT = 0 => NOTHING;
↑↑↑↑↑FOO\COUNT ∀← FOO\COUNT - 1;
↑↑↑↑↑εVε(FOO\SEM);
↑↑↑↑END
.endecl
.subsec etransreviveall,|Translation of /REVIVE(ALL ...)/|
There is a bit of difficulty with translating
/REVIVE(ALL#...)/: this is that the first
revived process may change the state of the system,
and so may the second, etc. That is, we cannot translate
/REVIVE(ALL#...)/ using a simple loop unless
and until it can be determined that the revived result
assertion will leave the state of the system as is.
Thus, it may be necessary to "unwrap" the standard
canned /STARTUP/ loop at the front, and code
the first few "iterations" specially. Eventually,
because the system has a finite number of states,
some state will recur and the loop will be closed.
Except for this problem, translation of
/REVIVE(ALL#...)/ is simply the obvious
"cross-product" of the translations of /REVIVE/
and of /STARTUP(ALL#...)/.
.subsec etransifposs,Translation of /IF ... POSSIBLE/
The /IF#...#POSSIBLE/ construct
may be translated exactly as in section @primifposs@.
Naturally, the embedded /STARTUP/ or
/REVIVE/ must be translated as described
in sections @etransstartup@-@etransreviveall@.
.subsec etranstry,Translation of /TRY ... END\TRY/
The /TRY/ construct will be translated
in precisely the manner described in section
@primtry@, using blocks containing conditionals.
.subsec etranseither,Translation of /EITHER ... OR ... END\OR/
The /EITHER/ construct will be translated
in precisely the manner described in section
@primtry@, using the hypothetical /SELECT/
statement.
.section extractexample,Example of Translation with Code Extraction
As an example of translation with code
extraction, let us consider just one more time
the priority exclusion problem of section
@mutexproblem@.
Recall that the state assertions for the problem were:
.beginecl
<↑LOCKED IS LOCK = TRUE,
↑UNLOCKED IS LOCK = FALSE,
↑HIGH\PRIORITY\PROCESS DOES
↑↑BEGIN
↑↑ASSERT(LOCKED, UNLOCKED);
↑↑CIA("HIGH\PRIORITY\WAIT");
↑↑ASSERT(UNLOCKED ==> LOCKED, ELSE WAIT);
↑↑IE "HACK DATA BASE";
↑↑ASSERT(LOCKED);
↑↑CIA("HIGH\PRIORITY\RELEASE");
↑↑ASSERT(ALWAYS UNLOCKED THEN
↑↑↑↑TRY IF REVIVE(HIGH\PRIORITY\PROCESS) POSSIBLE
↑↑↑↑NEXT IF REVIVE(LOW\PRIORITY\PROCESS) POSSIBLE
↑↑↑↑END\TRY);
↑↑END,
↑LOW\PRIORITY\PROCESS DOES
↑↑BEGIN
↑↑ASSERT(LOCKED, UNLOCKED);
↑↑CIA("LOW\PRIORITY\WAIT");
↑↑ASSERT(UNLOCKED ==> LOCKED, ELSE WAIT);
↑↑IE "HACK DATA BASE";
↑↑ASSERT(LOCKED);
↑↑CIA("LOW\PRIORITY\RELEASE");
↑↑ASSERT(ALWAYS UNLOCKED THEN
↑↑↑↑TRY IF REVIVE(HIGH\PRIORITY\PROCESS) POSSIBLE
↑↑↑↑NEXT IF REVIVE(LOW\PRIORITY\PROCESS) POSSIBLE
↑↑↑↑END\TRY);
↑↑END >
.endecl
The code generated by the SAL synthesizer is:
.beginecl
↑HIGH\PRIORITY\WAIT ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑LOCK = FALSE => LOCK ∀← NOT LOCK;
↑↑↑↑ENTERL(LASTRUN, HIGH\PRIORITY\PROCESS);
↑↑↑↑LASTRUN ∀← NIL;
↑↑↑END;
.endecl
.beginecl
↑HIGH\PRIORITY\RELEASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑HIGH\PRIORITY\PROCESS α# NIL =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑LASTRUN α# NIL -> ENTERL(LASTRUN, INACTIVEQ);
↑↑↑↑↑↑LASTRUN ∀← REMOVEF(HIGH\PRIORITY\PROCESS);
↑↑↑↑↑↑HIGH\PRIORITY\WAIT();
↑↑↑↑↑END;
↑↑↑↑LOW\PRIORITY\PROCESS α# NIL =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑LASTRUN α# NIL -> ENTERL(LASTRUN, INACTIVEQ);
↑↑↑↑↑↑LASTRUN ∀← REMOVEF(LOW\PRIORITY\PROCESS);
↑↑↑↑↑↑LOW\PRIORITY\WAIT();
↑↑↑↑↑END;
↑↑↑END;
.endecl
.beginecl
↑LOW\PRIORITY\WAIT ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑LOCK = FALSE => LOCK ∀← NOT LOCK;
↑↑↑↑ENTERL(LASTRUN, LOW\PRIORITY\PROCESS);
↑↑↑↑LASTRUN ∀← NIL;
↑↑↑END;
.endecl
.beginecl
↑LOW\PRIORITY\RELEASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑HIGH\PRIORITY\PROCESS α# NIL =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑LASTRUN α# NIL -> ENTERL(LASTRUN, INACTIVEQ);
↑↑↑↑↑↑LASTRUN ∀← REMOVEF(HIGH\PRIORITY\PROCESS);
↑↑↑↑↑↑HIGH\PRIORITY\WAIT();
↑↑↑↑↑END;
↑↑↑↑LOW\PRIORITY\PROCESS α# NIL =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑LASTRUN α# NIL -> ENTERL(LASTRUN, INACTIVEQ);
↑↑↑↑↑↑LASTRUN ∀← REMOVEF(LOW\PRIORITY\PROCESS);
↑↑↑↑↑↑LOW\PRIORITY\WAIT();
↑↑↑↑↑END;
↑↑↑END;
.endecl
Now we translate this code into semaphore code
using code extraction:
.beginecl
↑HIGH\PRIORITY\WAIT ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK = FALSE =>
↑↑↑↑↑↑[) LOCK ∀← NOT LOCK;
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(HIGH\PRIORITY\PROCESS\SEM);
↑↑↑END;
.endecl
.beginecl
↑HIGH\PRIORITY\RELEASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT GT 0 =>
↑↑↑↑↑↑[) HIGH\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT - 1;
↑↑↑↑↑↑ IE "WE ARE IN UNLOCKED STATE, HENCE EXTRACT
↑↑↑↑↑↑↑↑CODE FOR UNLOCKED STATE AND PUT HERE";
↑↑↑↑↑↑ LOCK ∀← NOT LOCK;
↑↑↑↑↑↑ εVε(HIGH\PRIORITY\PROCESS\SEM);
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑LOW\PRIORITY\PROCESS\COUNT GT 0 =>
↑↑↑↑↑↑[) LOW\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑↑↑LOW\PRIORITY\PROCESS\COUNT - 1;
↑↑↑↑↑↑ IE "EXTRACTED CODE ALSO PUT HERE (IT COMES
↑↑↑↑↑↑↑↑FROM A DIFFERENT FUNCTION, BUT HAPPENS
↑↑↑↑↑↑↑↑TO BE THE SAME)";
↑↑↑↑↑↑ LOCK ∀← NOT LOCK;
↑↑↑↑↑↑ εVε(LOW\PRIORITY\PROCESS\SEM);
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
.beginecl
↑LOW\PRIORITY\WAIT ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK = FALSE =>
↑↑↑↑↑↑[) LOCK ∀← NOT LOCK;
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑LOW\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑LOW\PRIORITY\PROCESS\COUNT + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(LOW\PRIORITY\PROCESS\SEM);
↑↑↑END;
.endecl
.beginecl
↑LOW\PRIORITY\RELEASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑TAG4:
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT GT 0 =>
↑↑↑↑↑↑[) HIGH\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑↑↑HIGH\PRIORITY\PROCESS\COUNT - 1;
↑↑↑↑↑↑ IE "EXTRACTED CODE HERE";
↑↑↑↑↑↑ LOCK ∀← NOT LOCK;
↑↑↑↑↑↑ εVε(HIGH\PRIORITY\PROCESS\SEM);
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑LOW\PRIORITY\PROCESS\COUNT GT 0 =>
↑↑↑↑↑↑[) LOW\PRIORITY\PROCESS\COUNT ∀←
↑↑↑↑↑↑↑↑LOW\PRIORITY\PROCESS\COUNT - 1;
↑↑↑↑↑↑ IE "EXTRACTED CODE HERE TOO";
↑↑↑↑↑↑ LOCK ∀← NOT LOCK;
↑↑↑↑↑↑ εVε(LOW\PRIORITY\PROCESS\SEM);
↑↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
This is quite simple and straightforward;
the system is "obviously"⊗⊗Handwave, handwave.⊗
always in the correct state, and slip-through cannot
occur since, as with the /urgentcount/ method,
a εVε is never done on the semaphore /mutex/
until the "original outermost" synchronization
function has completed.
.chapter chapbug,An Even More Subtle Bug
There is yet another subtle problem
with the code extraction technique of
semaphore code generation; this problem was
alluded to earlier. What is astounding is that
this problem did not arise in several months
of working with SAL code and semaphore
generation, and even then only in a "thought
experiment". The bug, however, is of quite
a serious nature and most certainly requires
solution before the code extraction approach
can be certified useable.
.section bugproblem,The Bug
The bug occurs, oddly enough, in the translation
of the /REVIVE/ action.
The problem has to do with the
extraction of code. Suppose that two or more different
synchronization functions perform /WAIT/
actions on the same waitset.
The question arises, from which function should
the code for a /REVIVE/ be extracted?
If the code to be extracted from the several
functions is identical for each function, then
there is no problem; one copy of the extracted
code will suffice, and perform the correct
state change.⊗⊗Historical note: when this bug
was first encountered the specific synchonization
problems at hand indeed had this property, and so
the bug was dismissed with a wave of the hand.
It returned later, however, to haunt another
synchronization program, and only then was
its seriousness realized fully.⊗
If the code for the two functions differ, however,
there is no immediate good answer to the problem,
and in fact the code extraction technique fails.
One might suggest extracting the code from the
various functions and determining at run time
which state changes to effect, but unfortunately
there is no way to tell what process the
εVε on the waitset-semaphore will release.
.section bugsolutions,Possible Solutions
Fortunately, the code extraction technique
is not a total loss; there are ways to fix
up the bug, though with clumsiness approximately
equal to that of the /urgentcount/
scheme.⊗⊗We may, on the other hand,
take comfort from the fact that a large
number of syncronization problems in practice do not
encounter this bug to begin with.⊗
.subsec bugsolncaveat,Caveat Emptor Again
As mentioned in section @solnloser@,
one way to fix a bug is to forbid the circumstances
which produce it. Indeed, the bug only potentially occurs
in well-defined circumstances, namely the case that
a waitset is mentioned in /WAIT/ actions
in more than one result assertion.
Thus we might avoid the bug by requiring a waitset
to appear in no more than one /WAIT/ action,
for example.
We may well ask, then, whether this will
unduly restrict the SAL user.
It in fact turns out that it does not, thanks to
the /EITHER/ construct.
Suppose, for example, that the following result
assertions appeared for various synchronization
functions in a system:
.beginecl
ASSERT(QUIESCENT ==> READING,
ELSE WAIT IN FOO);
ASSERT(QUIESCENT ==> WRITING,
ELSE WAIT IN FOO);
ASSERT(ALWAYS QUIESCENT THEN
TRY IF REVIVE(PROCESS OUTOF FOO) POSSIBLE END\TRY);
.endecl
The user could rewrite these assertions to avoid
the multiple usage of the waitset /FOO/ by using
the /EITHER/ construct:
.beginecl
ASSERT(QUIESCENT ==> READING,
ELSE WAIT IN FOO1);
ASSERT(QUIESCENT ==> WRITING,
ELSE WAIT IN FOO2);
ASSERT(ALWAYS QUIESCENT THEN
TRY EITHER IF REVIVE(PROCESS OUTOF FOO1) POSSIBLE
OR IF REVIVE(PROCESS OUTOF FOO2) POSSIBLE
END\TRY);
.endecl
Empirically, it seems to be reasonable to expect waitsets
to be "private" to a given process at a particular
point; see, for example, Dijkstra's discussion
in the appendix to [{THEsystem}]. (In fact, the SAL
synthesizer may impose this restriction for other reasons,
though this issue is not yet clear.)
.subsec bugsolnsplit,Waitset Splitting
The solution of section @bugsolncaveat@
suggests a way to fix the bug without burdening the
poor user. Since the circumstances under which the
bug potentially occurs are well defined, they can be
detected and fixed mechanically. That is, there is no
reason the translator cannot detect the multiple uses
of a waitset, "split" the waitset into several waitsets
each of which is used in one place, and generate the
correct set of /either/ constructs wherever a
/REVIVE/ action on the original waitset
occurs. This technique, while clumsy,
restores the integrity of the code extraction
technique and will be, we may hope, seldom used
in practice.
.section bughelpswait,A Solution to the α`α`Extracted /WAIT/'' Problem
In section @solnextract@ we raised the problem of what
to do if in the code extracted for a /REVIVE/ there is a /WAIT/
action. Certainly the reviving process cannot perform the /WAIT/!
The considerations of the present chapter, however, lead to
a more or less straightforward solution.
The idea is that if waitset semaphores are not to correspond
in a one-to-one manner with waitsets, then we may rearrange their
usage and use a single semaphore to represent several waitsets!
To be more explicit, rather than associating a semaphore
with each waitset, we will associate one semaphore
with each result assertion which contains
(one or more) /WAIT/ actions.⊗⊗This usage is precisely in
the spirit discussed by Dijkstra in the appendix to
[{THEsystem}].⊗
When extracting the code for a /REVIVE/, the /WAIT/ operation
will not be extracted; furthermore, the εVε operation
on the "released waitset" will be omitted. Thus the
waiting process is not allowed to proceed at all;
it is only "logically" moved from one waitset to the other.
Thus, for example, if a process /A/ is waiting in waitset
/FOO/, and is thereby hanging on semaphore
/A\FOO\SEM/, and process /B/ wishes to
cause it to be in waitset /BAR/, then process
/B/ does not perform ↓_εVε_↓/(A\FOO\SEM)/
as it ordinarily would for a /REVIVE/, but
rather leaves /A/ hanging on /A\FOO\SEM/,
and records the fact that process /A/ is really
in waitset /BAR/.
The "reviving" process will of course make the relevant state
variable changes. It may be necessary to introduce
some extra variables to keep track of what processes are in
which waitsets when waiting processes
are logically switched between waitsets in this manner.
.chapter chapoptimize,Optimization Techniques
In this chapter we will consider the
problem of optimizing semaphore code.
We will consider the reasons why such optimization
should be applied to the code generated from
the output of the SAL synthesizer,
the optimization techniques themselves,
and the particular circumstances which motivate
the application of each technique.
.section optwhy,Why Should We Optimize?
The translation techniques outlined in chapter
@chapextract@ will by themselves produce workable
semaphore code implementing the original synchronization
assertion specifications. However, the code produced is
utterly cretinous by the standards of code produced by
human programmers. It is not unusual for the straightforward
semaphore translation to produce code which is an order of
magnitude or more larger in size than equivalent human-generated
code. Furthermore, many of the variables introduced to keep track
of the number of processes in a waitset will typically
merely duplicate equivalent information contained in the user-declared
state variables. Finally, much useless or redundant code
may exist in the translation which could potentially be eliminated
on the basis of the state assertions provided by the user.
.section optwhat,What Should We Optimize?
On the basis of the preceding discussion,
it is evident that we should optimize primarily for
space gains, i.e. reduction firstly of the amount of
code, secondly of the number of state variables,
and thirdly of the number of semaphores.⊗⊗If semaphores
are implemented in a space-expensive manner, such
as using process queues internal to a time-sharing system,
reducing the number of semaphores may be of greater
importance than reducing the number of state variables.⊗
Such space reductions will probably produce marginal
time gains also, but this should not be a primary
consideration.
We will not be concerned here with machine-specific
optimizations such as "peephole" optimization of machine-language
instructions; all of our optimizations will be carried
out in the language output by the SAL synthesizer (i.e., EL1).
.section opthow,How Can We Optimize?
Let us now consider a number of methods we can use
in order to optimize the semaphore code. We will find that
the optimization techniques will be based on three different
kinds of knowledge about the code to be optimized.
The first kind is general knowledge about procedures:
effects of conditional expressions and
assignment statements, equivalence transformations on code
such as statement re-ordering within a block, merging of
equivalent code sequences, etc.
This knowledge is necessary to almost any program which
purports to deal with other programs; in particular,
standard kinds of optimizing compilers contain such knowledge.
The second kind of knowledge is that specific to
semaphores: that εPε operations may cause delays, that
εVε operations potentially unhang other processes,
that a semaphore can be modeled as an integer variable, etc.
This is application-specific knowledge, peculiar to the
optimizer we wish to construct.
The third kind of knowledge is possibly the most valuable
of all: the invariant assertions made by the user (and perhaps
verified by the assertion analyzer [{patsthesis}]), plus the relatively
tight constraints on code generated by the synthesizer.
The primary reason that we can perform so much optimization
on our generated code is that we are working within an
extremely well-defined problem domain. For each synchronization
function we have a declaration as to possible system states,
and thus some constraints on the values of state variables.
Furthermore we have the knowledge that only relatively
simple constructs are used in the generated code;
no procedure calls are involved, no fluidly bound variables,
no side effects other than assignment and semaphore primitives,
and no expressions involving other than simple arithmetic and
Boolean operations. When used to advantage this information
can easily permit the collapsing of code size by an order
of magnitude or more.
It should be stated here that one assumption has been
made implicitly which deserves to be justified; namely,
the assumption that a significant amount of optimization
can be achieved primarily by means of a series of small, local code
transformations. This is by no means an intuitively obvious
fact, and indeed we shall find that in some cases some global
analysis is needed. There are, however, at least two justifications for this
assumption. One is that to a large extent the user who writes
the state assertions and the verifier which verifies these assertions
together perform much of the necessary global analysis before
the optimizer (or even the semaphore code generator) is put to work.
The other is the "proof of pudding" justification that indeed in practice
these techniques produce astonishing condensation of actual code
produced by the semaphore code generator from the output of the
SAL synthesizer; this will be seen later in chapter @chapexamples@.
Let us then proceed to consider various kinds of code
transformations we can use to achieve code condensation, and at the
same time consider what kind of knowledge is neede to perform
these transformations.
.subsec optsimp,Simplification of Expressions
It is not unusual to see in the generated semaphore
code such expressions as:
.beginecl
↑↑VAR1 = 0 AND VAR2 = 0 OR VAR1 α# 0 AND VAR2 = 0
.endecl
It is clear that we will need an expression simplifier
with some knowledge about arithmetic and Boolean expressions.
Such a simplifier should not be too difficult to design,
since the expressions generated by the SAL synthesizer
contain no operations more complicated than integer arithmetic,
Boolean operators, and relational operators.
For example, we would expect the expression simplifier to be
capable of simplifying these expressions:
.beginecl
↑↑FOO + 1 + 2
↑↑FOO + 1 - 2
↑↑FOO + BAR - FOO + (BAR - (BAR - 1)) * QUUX
↑↑NOT NOT WALDO
↑↑FOO AND FROTZ OR FOO AND NOT FROTZ
↑↑VAR1 = 0 AND VAR2 = 0 OR VAR1 α# 0 AND VAR2 = 0
.endecl
into these expressions:
.beginecl
↑↑FOO + 3
↑↑FOO - 1
↑↑BAR + QUUX
↑↑WALDO
↑↑FOO
↑↑VAR2 = 0
.endecl
This kind of simplification is standard in many optimizing
compilers, not to mention symbolic manipulation systems
such as MACSYMA [{macsymamanual}].
Often we will be able to make simplifications
on the basis of known possible values for variables;
such information may come from the assertions
made by the user, or from the predicates of conditionals.
For example, suppose that it is known that /WALDO#=#TRUE/
and /FOO#≥#0/ when the following piece of code is entered:
.beginecl
↑BEGIN
↑↑WALDO ∀← WALDO AND NOT FROTZ;
↑↑FOO = 0 => [) BAR ∀← FOO + 1 (];
↑↑WALDO AND FOO GT 0 => [) BAR ∀← 0 (];
↑END
.endecl
Then it can be determined that /WALDO#=#TRUE/ when
the right-hand side of the first assignment is performed,
that /FOO#=#0/ when the assignment to /BAR/ occurs,
and that /FOO#>#0/ when the third statement is performed.
This information can be used to simplify the expressions
as follows:
.beginecl
↑BEGIN
↑↑WALDO ∀← NOT FROTZ;
↑↑FOO = 0 => [) BAR ∀← 1 (];
↑↑WALDO => [) BAR ∀← 0 (];
↑END
.endecl
.subsec optcond,Elimination of Useless Conditionals
If the predicate of a conditional is by some
means simplified to a constant (/TRUE/ or /FALSE/), then
the conditional may be eliminated in an appropriate manner.
This situation often occurs when code is extracted
for the translation of /REVIVE/.
If the predicate simplifies to /FALSE/, then the conditional
expression may simply be excised from the code.
If the predicate simplifies to /TRUE/, then the conditional
is replaced by the conditional's consequent expression;
furthermore, if the conditional is /=>/ rather than /->/,
all following statements in the block must be excised.
.subsec optmotion,Code Motion
Code motion is a standard technique familiar to those
who work with ordinary optimizing compilers.
The principle is that pieces of code may be moved about
relative to one another as long as the total effect
of the code remains the same. We will distinguish here
between two varieties of code motion.
The first variety involves
permuting the order of of a set of statements which are
such that any side effects of one do not affect execution
of any of the others.⊗⊗Such a set in fact has the property
that all the statements could be executed in parallel
if desired, though that really does not concern us here.⊗
For example:
.beginecl
↑BEGIN
↑↑FOO ∀← 43;
↑↑BAR ∀← 27;
↑END
.endecl
could be transformed into:
.beginecl
↑BEGIN
↑↑BAR ∀← 27;
↑↑FOO ∀← 43;
↑END
.endecl
if such a transformation were desirable. This kind of
code motion does not truly optimize the code, but may
be used in preparation for other transformations
which do optimize.
The second variety of code motion involves noting the
interdependence of two statements and adjusting the
statements to allow for the perturbation of their order.
This will often be possible inasmuch as the code we are concerned
with involves only a few well-understood constructs such
as simple arithmetic and assigments to simple variables.
As an example, in this code:
.beginecl
↑BEGIN
↑↑FOO ∀← FOO + 1;
↑↑BAR ∀← FOO - 1;
↑END
.endecl
the two assignments may be interchanged, because the
side effect of the first assignment may be compensated for:
.beginecl
↑BEGIN
↑↑BAR ∀← (FOO + 1) - 1;
↑↑FOO ∀← FOO + 1;
↑END
.endecl
which then in turn simplifies arithmetically to:
.beginecl
↑BEGIN
↑↑BAR ∀← FOO;
↑↑FOO ∀← FOO + 1;
↑END
.endecl
which provides some actual savings of code.
Similarly, if an assignment and a conditional are interchanged,
the predicate of the conditional may be modified to account
for the switch:
.beginecl
↑BEGIN
↑↑WALDO ∀← NOT WALDO
↑↑FOO = 0 OR NOT WALDO -> [) FOO ∀← 1; εVε(sem) (];
↑END
.endecl
may be transformed into:
.beginecl
↑BEGIN
↑↑FOO = 0 OR NOT (NOT WALDO) -> [) FOO ∀← 1; εVε(sem) (];
↑↑WALDO ∀← NOT WALDO
↑END
.endecl
which in turn simplifies into:
.beginecl
↑BEGIN
↑↑FOO = 0 OR WALDO -> [) FOO ∀← 1; εVε(sem) (];
↑↑WALDO ∀← NOT WALDO
↑END
.endecl
Again, note that this variety of code motion in itself
does not optimize the size of the program, but rather
may merely lead up to other simplifications.
.subsec optsplit,Code Splitting
This transformation is a kind of code motion
in which a piece of code is duplicated and moved
from outside a conditional into the arms of the conditional.
For example:
.beginecl
↑BEGIN
↑↑FOO ∀← FOO + 1;
↑↑WALDO => [) BAR ∀← 3 (];
↑↑BAR ∀← 4;
↑END
.endecl
may be transformed into:
.beginecl
↑BEGIN
↑↑WALDO => [) FOO ∀← FOO + 1; BAR ∀← 3 (];
↑↑FOO ∀← FOO + 1;
↑↑BAR ∀← 4;
↑END
.endecl
This is in fact a $dis$optimizing transformation since it
makes the code larger! Such a splitting of code may be justified,
however, if it leads to greater optimization within one or
more arms of the conditional. Code splitting in fact often
leads to the use of code merging or code cancellation
(see sections @optmerge@ and @optcancel@).
As for ordinary code motion, it may be necessary
to modify the predicate of the conditional to account for side
effects if the split statement is moved past it.
Code splitting may also be performed with
respect to the /SELECT/ statement, which is
after all also a conditional. For example,
the following code:
.beginecl
↑BEGIN
↑↑FOO ∀← FOO + 1;
↑↑SELECT
↑↑↑[FOO GT 0]
↑↑↑↑↑[) εVε(FOO\SEM);
↑↑↑↑↑ εVε(mutex) (];
↑↑↑[BAR GT 0]
↑↑↑↑↑[) εVε(BAR\SEM);
↑↑↑↑↑ εVε(mutex) (];
↑↑END;
↑END
.endecl
could be transformed via code splitting into this
(with an appropriate alteration of one predicate
because of code motion):
.beginecl
↑BEGIN
↑↑SELECT
↑↑↑[FOO GT -1]
↑↑↑↑↑[) FOO ∀← FOO + 1;
↑↑↑↑↑ εVε(FOO\SEM);
↑↑↑↑↑ εVε(mutex) (];
↑↑↑[BAR GT 0]
↑↑↑↑↑[) FOO ∀← FOO + 1;
↑↑↑↑↑ εVε(BAR\SEM);
↑↑↑↑↑ εVε(mutex) (];
↑↑END;
↑END
.endecl
.subsec optmerge,Code Merging
Code merging is the transformation inverse to
code splitting; namely, a statement common to all arms
of a conditional may be removed from all arms
and placed outside the conditional. More specifically,
if the common statement appears at the beginning
of each arm, it may be moved to a point just before the
conditional;
if the common statement appears at the end of
each arm, it may be placed after the conditional.
In the first case the predicate of the conditional
may have to be adjusted to account for side effects.
If the common statement appears at odd places in each arm,
code motion may be used within each arm to get the statements
to the required positions.
For example:
.beginecl
↑BEGIN
↑↑FOO = 0 => [) BAR ∀← 1;
↑↑ FOO ∀← FOO + 1;
↑↑ QUUX ∀← 3 (];
↑↑FOO ∀← FOO + 1;
↑END
.endecl
could be optimized in one of two ways. The first occurrence
of /FOO/↓_#∀←#_↓/FOO#+#1/ could be moved to the beginning of its arm:
.beginecl
↑BEGIN
↑↑FOO = 0 => [) FOO ∀← FOO + 1;
↑↑ BAR ∀← 1;
↑↑ QUUX ∀← 3 (];
↑↑FOO ∀← FOO + 1;
↑END
.endecl
and then merged in front of the conditional, adjusting the predicate:
.beginecl
↑BEGIN
↑↑FOO ∀← FOO + 1;
↑↑FOO = 1 => [) BAR ∀← 1;
↑↑ QUUX ∀← 3 (];
↑END
.endecl
Alternatively, the first occurrence
of /FOO/↓_#∀←#_↓/FOO#+#1/ could be moved to the end of its arm:
.beginecl
↑BEGIN
↑↑FOO = 0 => [) BAR ∀← 1;
↑↑ QUUX ∀← 3;
↑↑ FOO ∀← FOO + 1 (];
↑↑FOO ∀← FOO + 1;
↑END
.endecl
and then merged following the conditional:
.beginecl
↑BEGIN
↑↑[) FOO = 0 => [) BAR ∀← 1;
↑↑ QUUX ∀← 3 (] (];
↑↑FOO ∀← FOO + 1;
↑END
.endecl
(The EL1 syntax for conditionals is unfortunately
asymmetric, as opposed to the /IF ... THEN ... ELSE ... FI/
construct of Algol, and so we have had to introduce
an extra set of /[) (]/ brackets to perform the transformation.
It is assumed that our optimizer understands this problem
and is capable of introducing and expunging block structure
as necessary.
Thus in fact the above code could be textually simplified further:
.beginecl
↑BEGIN
↑↑FOO = 0 -> [) BAR ∀← 1;
↑↑ QUUX ∀← 3 (];
↑↑FOO ∀← FOO + 1;
↑↑END
.endecl
by use of the /->/ operator. This is of course not an
optimization, but merely an abbreviation which makes it more
readable.)
Code merging may also be performed with respect
to /SELECT/ statements, just as code splitting may.
For example, the following block of code:
.beginecl
↑BEGIN
↑↑SELECT
↑↑↑[FOO GT 0]
↑↑↑↑↑[) FOO ∀← FOO - 1;
↑↑↑↑↑ εVε(FOO\SEM);
↑↑↑↑↑ εVε(mutex) (];
↑↑↑[BAR GT 0]
↑↑↑↑↑[) FOO ∀← FOO - 1;
↑↑↑↑↑ εVε(BAR\SEM);
↑↑↑↑↑ εVε(mutex) (];
↑↑END;
↑END
.endecl
may be transformed by using two code mergings (and
adjusting one predicate appropriately) into this code:
.beginecl
↑BEGIN
↑↑FOO ∀← FOO - 1;
↑↑SELECT
↑↑↑[FOO GT -1]
↑↑↑↑↑[) εVε(FOO\SEM) (];
↑↑↑[BAR GT 0]
↑↑↑↑↑[) εVε(BAR\SEM) (];
↑↑END;
↑↑εVε(mutex);
↑END
.endecl
.subsec optcancel,Code Cancellation
Sometimes the effects of two pieces of code may
cancel each other, or one may supersede the effects of the other.
This often happens when code is extracted from another
synchronization function and the extracted code returns the
system to a former state or new state.
In such a circumstance the cancelling or superseded code
may be excised. Often such cancellations
will use the fact that an occurrence of
/(FOO#/↓_∀←_↓/#FOO)/
is equivalent to an occurrence of merely /FOO/,
and also that /FOO/ as a statement in a block
has no effect at all unless it is the last statement
(and thus represents the value of the block).
For example:
.beginecl
↑BEGIN
↑↑FOO ∀← FOO + 1;
↑↑FOO ∀← FOO - 1;
↑↑QUUX ∀← QUUX + 1;
↑↑QUUX ∀← QUUX - 2;
↑↑BAR ∀← BAR + 1;
↑↑BAR ∀← 3;
↑END
.endecl
simplifies into this:
.beginecl
↑BEGIN
↑↑FOO ∀← (FOO + 1) - 1;
↑↑QUUX ∀← (QUUX + 1) - 2;
↑↑BAR ∀← 3;
↑END
.endecl
and then, by simplification of expressions, into this:
.beginecl
↑BEGIN
↑↑FOO ∀← FOO;
↑↑QUUX ∀← QUUX - 1;
↑↑BAR ∀← 3;
↑END
.endecl
and finally, by simplification and elimination of
the useless assignment /(FOO#/↓_∀←_↓/#FOO)/:
.beginecl
↑BEGIN
↑↑QUUX ∀← QUUX - 1;
↑↑BAR ∀← 3;
↑END
.endecl
Sometimes code motion and code splitting
may be necessary in order to cancel the code:
.beginecl
↑BEGIN
↑↑FOO ∀← FOO + 1;
↑↑WALDO => [) BAR ∀← 3;
↑↑ FOO ∀← FOO - 1 (];
↑↑BAR ∀← 2;
↑END
.endecl
may first be transformed by splitting the statement /FOO/↓_#∀←#_↓/FOO#+#1/
into the conditional:
.beginecl
↑BEGIN
↑↑WALDO => [) FOO ∀← FOO + 1;
↑↑ BAR ∀← 3;
↑↑ FOO ∀← FOO - 1 (];
↑↑FOO ∀← FOO + 1;
↑↑BAR ∀← 2;
↑END
.endecl
then by permuting two assignments:
.beginecl
↑BEGIN
↑↑WALDO => [) BAR ∀← 3;
↑↑ FOO ∀← FOO + 1;
↑↑ FOO ∀← FOO - 1 (];
↑↑FOO ∀← FOO + 1;
↑↑BAR ∀← 2;
↑END
.endecl
and finally by cancelling the first two assignments to /FOO/:
.beginecl
↑BEGIN
↑↑WALDO => [) BAR ∀← 3 (];
↑↑FOO ∀← FOO + 1;
↑↑BAR ∀← 2;
↑END
.endecl
.subsec optequiv,Equivalence Transformations
Under certain circumstances, two pieces of code
which normally are not equivalent may be shown to be
equivalent on the basis of extra state information.
The SAL synthesizer is in fact aware of this fact already,
in that it may have a choice of how to express as assignment
to a state variable, and must choose one or the other.
For example, the two statements:
.beginecl
↑↑↑WALDO ∀← FALSE
↑↑↑WALDO ∀← NOT WALDO
.endecl
are ordinarily not equivalent in their effects.
If it is known, however, that when the statement is
to be executed /WALDO/ must always be /TRUE/,
then the two statements are indeed equivalent.
The optimizer often needs to understand such
equivalences in order to perform code merging and
code cancellation. Typically, the optimizer might
spot two assignments to the same variable, and notice
that they are candidates for merging except that
the right-hand sides differ. If the optimizer could
prove that the effects would be the same if one of
them were altered to have the other's form,
then it could perform the transformation and subsequently
merge or cancel the code. For example, in the following code:
.beginecl
↑BEGIN
↑↑WALDO = TRUE =>
↑↑↑[) TGQ ∀← 43;
↑↑↑ WALDO ∀← FALSE (];
↑↑WALDO ∀← NOT WALDO;
↑END
.endecl
the assignment /WALDO#/↓_∀←_↓/#FALSE/ occurs only when
it is known that /WALDO = TRUE/; in these circumstances
the assignment /WALDO#/↓_∀←_↓/#NOT WALDO/ would do just
as well.
.beginecl
↑BEGIN
↑↑WALDO = TRUE =>
↑↑↑[) TGQ ∀← 43;
↑↑↑ WALDO ∀← NOT WALDO (];
↑↑WALDO ∀← NOT WALDO;
↑END
.endecl
Now it is possible to merge the two assignments to /WALDO/:
.beginecl
↑BEGIN
↑↑WALDO = FALSE => TGQ ∀← 43;
↑↑WALDO ∀← NOT WALDO;
↑END
.endecl
This technique is particularly powerful in our situation
because we have a great deal of information initially
regarding the possible values of variables; this information
comes from the state assertions made by the user.
.subsec optvars,Removal of Unnecessary Variables
Intuitively, it it seems that in general it
should be possible to remove all occurrences
of a variable if that variable does not really affect the
workings of the system. It is difficult, however,
to characterize precisely
what this means. Since we are here concerned with output of
the SAL synthesizer, we may assume that the only
constructs we have to worry about are assignments,
simple arithmetic, built-in predicates such as /GT/,
and primitive control structures such as /=>/ and /SELECT/;
arbitrary and unknown user functions are not permitted.
As a first approximation, let us define a
variable to be unnecessary if it never appears in the
predicate of a conditional. This appears to be obvious,
but is not quite correct. A variable could still affect a system
if it affected another variable which in turn appeared in
a predicate. For example:⊗⊗In the examples in this section
each little block of code is to be taken as a complete and self-contained
system. In practice, of course, one must consider $all$ the synchronization
functions together in order to determine the useless variables,
because a variable which appears useless in one synchronization
function may affect another such function (that is, after all,
the entire point of having state variables!).⊗
.beginecl
↑BEGIN
↑↑QUUX ∀← WALDO - 3;
↑↑QUUX GT 0 => FROTZ;
↑↑WALDO ∀← QUUX * 2;
↑END
.endecl
The variable /WALDO/ appears in no predicate, yet manifestly
affects the system via the variable /QUUX/.
As a second approximation, then, let us define a
variable as useless if it does not appear in predicates
$and$ does not appear on the right hand side of any assignment.
Unfortunately, this takes us too far in the other direction;
i.e., this definition does not encompass all useless variables.
For example:
.beginecl
↑BEGIN
↑↑WALDO ∀← WALDO + 1;
↑↑QUUX GT 0 => FROTZ;
↑↑QUUX ∀← QUUX - 43;
↑END
.endecl
In this case /WALDO/ is indeed an unnecessary variable, even
though it appears in the right hand side of an assignment.
The problem is that the assignment is an assignment to
/WALDO/ itself, and not to a variable such as /QUUX/
which does affect the system.
Let us therefore, as a third approximation,
not call a variable necessary if it appears in the right
hand side of an assignment to itself.
This is not sufficient either:
.beginecl
↑BEGIN
↑↑WALDO ∀← QUUX + 1;
↑↑QUUX ∀← WALDO + 1;
↑↑FROTZ => BAR ∀← BAR + 1;
↑END
.endecl
In this example /WALDO/ appears to be necessary because it
affects /QUUX/, and /QUUX/ because it affects /WALDO/.
In fact, each variable $is$ individually necessary;
but taken together the two are collectively unnecessary!
We now have enough terms to guess the formula
for the limit of these approximations. We need to keep
some kind of global data base to determine which variables
ultimately affect the system, and which are unnecessary and
may be eliminated. Probably the way to do this is to use
a directed graph. Let there be a node for each variable,
and a node to represent the system.
For each assignment statement let there
be an arc from each variable on the right-hand side to the
variable on the left-hand side. For each conditional predicate
let there be an arc from each variable in the predicate
to each variable assigned within the consequent,
and also to each variable assigned after the conditional in the block
if the conditional is /=>/; let there be an arc directly to
the system node if there is a semaphore operation
in the consequent (or following the conditional in the case of /=>/).
Then a variable is necessary if and only if there is a path
in the directed graph from that variable's node to the node
representing the system.
Note that as code is moved and merged, and useless
conditionals removed, it may be necessary to reconstruct the
graph repeatedly. If the graph is properly represented, it may
be easier to modify the graph as other transformations are made
than to repeatedly reconstruct the graph from scratch.
I doubt that this technique is original with me,
but then I also suspect that in ordinary optimizing
compilers it is not carried out to its fullest rigor and extent.
For our purposes here, it is quite necessary to eliminate
$all$ unnecessary variables, for only by so doing can
we hope to eliminate /mutex/ (see section @optmutexelim@ below).
.subsec optmap,Data Mappings and Substitution of Variables
If enough information is known about the values
of variables in a given global state, it may be possible
to merge several variables into one variable, or to
eliminate a variable by deriving the information it contains
from other variables. (It often occurs that the state variables
declared by the user are redundant, or that the counters introduced
to keep track of the sizes of waitsets duplicate information
in the state variables.)
For example, suppose the following state information
is given by the user:
.beginecl
↑STATE1 IS WALDO = FALSE AND QUUX = 0
↑STATE2 IS WALDO = TRUE AND QUUX = 0
↑STATE3 IS WALDO = TRUE AND QUUX GE 0 AND FROB = 1
↑STATE4 IS WALDO = TRUE AND QUUX GT 0 AND FROB = 2
.endecl
From this information we can derive the following facts
about the two variables /QUUX/ and /WALDO/:
.beginecl
↑↑↑WALDO = FALSE ∀→ QUUX = 0
↑↑↑QUUX > 0 ∀→ WALDO = TRUE
.endecl
Then we may be able introduce a new variable /ZTESCH/ which can
reflect the information contained in both /QUUX/ and /WALDO/:
.beginecl
.tabs 10,18,26,34,42,50,58,66,74
QUUX↑0↑0↑1↑2↑3↑4↑5↑...
WALDO↑FALSE↑TRUE↑TRUE↑TRUE↑TRUE↑TRUE↑TRUE↑...
ZTESCH↑0↑1↑2↑3↑4↑5↑6↑...
.endecl
Thus we have the following relationships:
.beginecl
↑↑↑WALDO = FALSE ∀↔ ZTESCH = 0
↑↑↑WALDO = TRUE ∀↔ ZTESCH > 0
↑↑↑QUUX > N ∀↔ ZTESCH > N+1
.endecl
The variable substitution is then completed by using
these relationships to substitute expressions in
/ZTESCH/ for expressions in /QUUX/ or /WALDO/.
Similarly, suppose we have the following state information:
.beginecl
↑STATE1 IS FROB = FALSE AND MUNG = FALSE AND HACK = TRUE
↑STATE2 IS FROB = TRUE AND MUNG = FALSE AND HACK = FALSE
↑STATE3 IS FROB = FALSE AND MUNG = TRUE AND HACK = FALSE
.endecl
Then it is not difficult to show that:
.beginecl
FROB = TRUE ∀↔ MUNG = FALSE AND HACK = FALSE
.endecl
and therefore /FROB/ can be totally eliminated and replaced
with appropriate constructions involving /MUNG/ and /HACK/.
(One could even imagine replacing all three with a single
integer variable /FOO/ taking on the values /1/, /2/, and /3/;
but this would be considerably more difficult since there
is no straightforward way to represent, say, /MUNG#/↓_∀←_↓/#NOT#MUNG/
in terms of /FOO/.)
.subsec optsmotion,Semaphore Motion
This special case of code motion allows semaphore operations
to be moved relative to other code. It often involves changing
the initial value of the semaphore. This technique is
not general as optimizing techniques go, but rather is peculiar to
the problem of semaphore code generation, and depends greatly
on having knowledge of state changes in the synthesized code.
An example of the use of this technique will appear later
in section @exclusion@.
.next page << for footnote loss >>
.subsec optmutexelim,Elimination of /mutex/
This is a one-shot simplification which involves removing
all references to the semaphore /mutex/.
This can always be done if all variables
have been eliminated, leaving only semaphore
operations.⊗⊗No proof of this claim will be presented in this
thesis. The author spent some time trying to do so,
and in the process has developed a formalism for
expressing the effects of semaphore operations
in rigorous terms. An exposition of this formalism
and a proof of the claimed theorem may be the subject
of a future paper; the matter has turned out to be
much too complex to solve in the time available.⊗
A similar theorem, which may be useful in odd cases, is
that it is permissible to $tentatively$ remove /mutex/, if
so doing will ultimately facilitate the removal of all variables.
A third, which is useful if the second one applies,
is that if /mutex/ indeed can be removed, then it is not
necessary to extract all the state-changing code from the
revived process. This sometimes allows one to leave a variable
transformation in the revived process instead of the reviving
process, which may lead to further simplification
.subsec optmutexsplit,Splitting of /mutex/
The author has not yet explored this technique in any depth,
primarily because on the surface it does not gain anything in
the examples tried to date; hence it is mentioned here only
for speculative purposes. The essential idea is that some
marginal amount of efficiency may be gained by not locking out
the whole world in order to access
state variables, but only enough to get the job done.
(For example, it is ridiculous to prevent a routine which wants
to read from the disk from entering its synchronization function
merely because another is in a function which synchronizes
the line printer (unless the other is a line printer spooler...).)
The idea is that one can split /mutex/ into a number
of semaphores, and assign each semaphore to a group of
one or more variables. In order to access a certain
set of variables, it would be necessary and sufficient
to lock all those and only those variable classes which together contain
the relevant variables. Difficult problems arise in the ordering
of operations on these semaphores if deadlock is to be avoided.
.section optwhen,When Should We Optimize?
We have considered a large number of transformations
which we may apply to the generated semaphore code.
There still remains the problem of $motivation$:
at any given point in the optimization process, how
can we decide which transformation to apply next?
The question is important, not only for efficiency reasons,
but because of the potential for thrashing.
For example, if the techniques are not correctly motivated,
the optimizer could conceivably go into a loop,
splitting and merging code, or permuting statements
forever.
We will find it convenient to divide the transformations
into two classes. First, we will consider the class
of truly optimizing transformations:
.begin "temp47" group nofill
.indent 12,12
Simplification of expression
Elimination of useless conditionals
Code merging
Code cancellation
Equivalence transformations which reduce code
Removal of unnecessary variables
Data mappings which reduce the number of variables
Elimination of /mutex/
.end "temp47"
Second, we will consider the class of tentative intermediate
transformations:
.begin "temp56" group nofill
.indent 12,12
Code motion
Code splitting
Equivalence transformations which expand code
Data mappings which do not reduce variables
Semaphore motion
.end "temp56"
The first class of transformations is characterized
by the fact that the amount of code is reduced.⊗⊗This must
of course be defined in some appropriate sense, such as the number
of operators in the expression.⊗
Thus we may hope to guarantee that the optimizer does not
thrash by requiring that its primary goals be transformations
of the first class; second class transformations are to be
used only as subsidiary goals to aid the primary transformations.
Thus, for example, code splitting is not allowed for its own sake,
but is permissible if it will lead to code cancellation.
Naturally, some extra constraints are also needed; for example,
a code split must not be allowed merely because it will enable
the inverse code merge!
In the problem environment we have been considering,
where the code contains mostly assignment statements and
semaphore operations, deciding which transformations are
potentially applicable should not be too difficult.
The best candidates for code merging and code cancellation,
for example, are assignment statements with the same variable
on the left-hand side. Equivalence transformations
are primarily useful if they allow one assignment to
be transformed into the same form as another, so that they
may be merged or cancelled. Removal of unnecessary variables
should probably be performed when nothing else interesting can
be done immediately; useless variables are unlikely to occur until
after other simplifications have taken place.
Expression simplification should almost always be undertaken first.
If sufficient care is taken, then, the techniques can be applied
in a reasonable order and thrashing prevented.
.chapter chapexamples,Examples
In this chapter we will consider a number of examples
of the operation of the system composed of the SAL synthesizer,
the semaphore code generator (using code extraction), and
the semaphore code optimizer. For each example
the synchronization problem will first be defined;
following the problem definition will be a solution to
the problem in terms of SAL assertions.
Next will appear the code exactly as output by the SAL
synthesizer, followed by the output of the semaphore code
generator. Next we shall carefully consider the motivation
and application of various optimizations, one by one,
until a final solution which admits of no further useful
optimization is reached. At each step the tranformed functions
will be redisplayed, with a "%5|%*"
at the beginning of any line which has changed from the previous
display.
.section coroutines,Simple Coroutines
There are two processes, only one of which
runs at a time. When one process has run for a while,
it passes control to the other and waits until the other
passes control back, at which time it continues execution.
The SAL assertions for this problem are as follows:
.beginecl
<↑PROCESS\1\RUNNING IS SWITCH = 1,
↑PROCESS\2\RUNNING IS SWITCH = 2,
↑PROCESS\1 DOES
↑↑REPEAT
↑↑↑ASSERT(PROCESS\1\RUNNING);
↑↑↑CIA("PASS\TO\2");
↑↑↑ASSERT(ALWAYS PROCESS\2\RUNNING
↑↑↑↑↑↑AND WAIT
↑↑↑↑↑↑AND STARTUP(PROCESS\2));
↑↑↑IE "STUFF THAT PROCESS 1 DOES";
↑↑END,
↑PROCESS\2 DOES
↑↑REPEAT
↑↑↑ASSERT(PROCESS\2\RUNNING);
↑↑↑CIA("PASS\TO\1");
↑↑↑ASSERT(ALWAYS PROCESS\1\RUNNING
↑↑↑↑↑↑AND WAIT
↑↑↑↑↑↑AND STARTUP(PROCESS\1));
↑↑↑IE "STUFF THAT PROCESS 2 DOES";
↑↑END >
.endecl
(Note added in proof:
These assertions actually are not quite correct; Griffiths
points out that there is a problem with initializing the system.
We will not be concerned with this here, since it will not
affect the example. It should be noted, however, that the
correct assertion for the second process is:
.beginecl
↑PROCESS\2 DOES
↑↑BEGIN
↑↑↑ASSERT(PROCESS\1\RUNNING);
↑↑↑CIA("INITIALIZE\PROCESS\2");
↑↑↑ASSERT(ALWAYS WAIT);
↑↑↑REPEAT
↑↑↑↑ASSERT(PROCESS\2\RUNNING);
↑↑↑↑CIA("PASS\TO\1");
↑↑↑↑ASSERT(ALWAYS PROCESS\1\RUNNING
↑↑↑↑↑↑↑AND WAIT
↑↑↑↑↑↑↑AND STARTUP(PROCESS\1));
↑↑↑↑IE "STUFF THAT PROCESS 2 DOES";
↑↑↑END
↑↑END
.endecl
which provides for correctly starting up process 2 rather
than having to assume that is magically starts out in
the waitset.)
The SAL synthesizer produces from these assertions
the following code:
.beginecl
↑PASS\TO\1 ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑ENTERL(LASTRUN, PROCESS\2);
↑↑↑↑LASTRUN ∀← NIL;
↑↑↑↑SWITCH ∀← SWITCH - 1;
↑↑↑↑ENTERL(REMOVEF(PROCESS\1), INACTIVEQ);
↑↑↑END;
↑PASS\TO\2 ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑ENTERL(LASTRUN, PROCESS\1);
↑↑↑↑LASTRUN ∀← NIL;
↑↑↑↑SWITCH ∀← SWITCH + 1;
↑↑↑↑ENTERL(REMOVEF(PROCESS\2), INACTIVEQ);
↑↑↑END;
.endecl
Note that the manipulations of /SWITCH/, while not what a human
programmer might code, indeed do the correct thing.
Next we translate the synthesized CI code into
semaphore code:
.beginecl
↑PASS\TO\1 ∀←
↑↑EXPR()
↑↑↑BEGIN
∞↑↑↑εPε(mutex);
↑↑↑↑SWITCH ∀← SWITCH - 1;
∞↑↑↑εVε(PROCESS\2\SEM);
∞↑↑↑εVε(mutex);
∞↑↑↑εPε(PROCESS\1\SEM);
↑↑↑END;
↑PASS\TO\2 ∀←
↑↑EXPR()
↑↑↑BEGIN
∞↑↑↑εPε(mutex);
↑↑↑↑SWITCH ∀← SWITCH + 1;
∞↑↑↑εVε(PROCESS\1\SEM);
∞↑↑↑εVε(mutex);
∞↑↑↑εPε(PROCESS\2\SEM);
↑↑↑END;
.endecl
It is fairly easy to see at this point that /SWITCH/
is a useless variable. Assignments to it may therefore be totally
eliminated:
.beginecl
↑PASS\TO\1 ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
%5|%*
↑↑↑↑εVε(PROCESS\2\SEM);
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(PROCESS\1\SEM);
↑↑↑END;
↑PASS\TO\2 ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
%5|%*
↑↑↑↑εVε(PROCESS\1\SEM);
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(PROCESS\2\SEM);
↑↑↑END;
.endecl
At this point all state variables have been eliminated,
and so the operations on /mutex/ may also be eliminated
(see section @optmutexelim@):
.beginecl
↑PASS\TO\1 ∀←
↑↑EXPR()
↑↑↑BEGIN
%5|%*
↑↑↑↑εVε(PROCESS\2\SEM);
%5|%*
↑↑↑↑εPε(PROCESS\1\SEM);
↑↑↑END;
↑PASS\TO\2 ∀←
↑↑EXPR()
↑↑↑BEGIN
%5|%*
↑↑↑↑εVε(PROCESS\1\SEM);
%5|%*
↑↑↑↑εPε(PROCESS\2\SEM);
↑↑↑END;
.endecl
This code does not seem to admit of further optimization.
The techniques of chapter @chapoptimize@ have done away with
all the useless state variable and /mutex/ machinery, leaving
only the necessary semaphore operations.
Our final solution is therefore the following compact code:
.beginecl
↑PASS\TO\1 ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εVε(PROCESS\2\SEM);
↑↑↑↑εPε(PROCESS\1\SEM);
↑↑↑END;
↑PASS\TO\2 ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εVε(PROCESS\1\SEM);
↑↑↑↑εPε(PROCESS\2\SEM);
↑↑↑END;
.endecl
.section exclusion,Simple Mutual Exclusion
This example is the same as that used in section
@bruteexample@: all processes are alike,
and there is a data base to which no two processes may have
simultaneous access.
The assertions for the problem are as follows:
.beginecl
<↑UNLOCKED IS LOCK = 0,
↑LOCKED IS LOCK = 1,
↑SOMEBODY DOES
↑↑BEGIN
↑↑↑ASSERT(UNLOCKED, LOCKED);
↑↑↑CIA("LOCK\DATA\BASE");
↑↑↑ASSERT(UNLOCKED ==> LOCKED, ELSE WAIT);
↑↑↑"HACK DATA BASE";
↑↑↑ASSERT(LOCKED);
↑↑↑CIA("UNLOCK\DATA\BASE");
↑↑↑ASSERT(ALWAYS UNLOCKED THEN TRY
↑↑↑↑↑IF REVIVE(ARBITRARY\PROCESS) POSSIBLE
↑↑↑↑END\TRY);
↑↑END >
.endecl
The SAL synthesizer produces the following code from
these assertions:
.beginecl
↑LOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑LOCK = FALSE => LOCK ∀← NOT LOCK;
↑↑↑↑ENTERL(LASTRUN, SOMEBODY);
↑↑↑↑LASTRUN ∀← NIL;
↑↑↑END;
↑UNLOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑SOMEBODY α# NIL =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑LASTRUN α# NIL -> ENTERL(LASTRUN, INACTIVEQ);
↑↑↑↑↑↑LASTRUN ∀← REMOVEF(SOMEBODY);
↑↑↑↑↑↑LOCK\DATA\BASE();
↑↑↑↑↑END;
↑↑↑END;
.endecl
Next we translate the synthesized CI code into
semaphore code. We will do this in two steps;
the /REVIVE/ is not fully translated in this first step because
it is generally easier to do the necessary code extraction
after the other translations have been performed.
.beginecl
↑LOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
∞↑↑↑εPε(mutex);
∞↑↑↑LOCK = FALSE => [) LOCK ∀← NOT LOCK; εVε(mutex) (];
∞↑↑↑SOMEBODY\COUNT ∀← SOMEBODY\COUNT + 1;
∞↑↑↑εVε(mutex);
∞↑↑↑εPε(SOMEBODY\SEM);
↑↑↑END;
↑UNLOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
∞↑↑↑εPε(mutex);
↑↑↑↑LOCK ∀← NOT LOCK;
∞↑↑↑SOMEBODY\COUNT GT 0 =>
↑↑↑↑↑BEGIN
∞↑↑↑↑↑REVIVE(SOMEBODY);
∞↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
∞↑↑↑εVε(mutex);
↑↑↑END;
.endecl
Now we are ready to translate the /REVIVE/ construct.
The /REVIVE/ must expand into the appropriate εVε, and
must also use extracted code for changing the state variables.
In doing this extraction some elimination
of useless conditionals has been done on the basis of state information;
in actual practice this elimination could be done as a separate step,
and would indeed have to be done separately for full generality.
.beginecl
↑LOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK = FALSE => [) LOCK ∀← NOT LOCK; εVε(mutex) (];
↑↑↑↑SOMEBODY\COUNT ∀← SOMEBODY\COUNT + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(SOMEBODY\SEM);
↑↑↑END;
↑UNLOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑SOMEBODY\COUNT GT 0 =>
↑↑↑↑↑BEGIN
∞↑↑↑↑↑SOMEBODY\COUNT ∀← SOMEBODY\COUNT - 1;
∞↑↑↑↑↑LOCK ∀← NOT LOCK;
∞↑↑↑↑↑εVε(SOMEBODY\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
Next we shall find it convenient to use code motion and
code cancellation in order to simplify the manipulation of
the variable /LOCK/. This is motivated primarily by the
introduction of extra code which manipulates lock
by the previous (extraction) step. In order to perform
this code cancellation, the knowledge that /NOT NOT X ≡ X/
is needed.
.beginecl
↑LOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑LOCK = FALSE => [) LOCK ∀← NOT LOCK; εVε(mutex) (];
↑↑↑↑SOMEBODY\COUNT ∀← SOMEBODY\COUNT + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(SOMEBODY\SEM);
↑↑↑END;
↑UNLOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
%5|%*
↑↑↑↑SOMEBODY\COUNT GT 0 =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑SOMEBODY\COUNT ∀← SOMEBODY\COUNT - 1;
%5|%*
↑↑↑↑↑↑εVε(SOMEBODY\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
∞↑↑↑LOCK ∀← NOT LOCK;
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
Now we need some information about the behavior of the
variable /SOMEBODY\COUNT/. To do this we follow a procedure very much
like that used in the SAL verifier to determine the
possible values of variables; in fact, it may in practice
be possible to use the verifier's data base and routines for
this calculation.
For purposes of exposition we will find it convenient
to use a tabular format to display information as it is gleaned.
We assume that in the "initial" state⊗⊗It is not clear from
current descriptions of SAL exactly how the "initial state"
is determined.⊗
that generated semaphores are initially 0,
except /mutex/, which is initially 1.
Therefore our initial knowledge is as follows:
.beginecl
.tabs 11,26,36
↑↑LOCK↑SOMEBODY\COUNT
↑UNLOCKED↑FALSE↑ 0
↑LOCKED↑TRUE
.endecl
Examination of /LOCK\DATA\BASE/ when entered in the
/UNLOCKED/ state shows that a transition to the /LOCKED/ state
is possible without changing the value of /SOMEBODY\COUNT/.
Therefore any value possible in the former state is possible
in the latter.
.beginecl
.tabs 11,26,36
↑↑LOCK↑SOMEBODY\COUNT
↑UNLOCKED↑FALSE↑ 0
↑LOCKED↑TRUE↑ 0
.endecl
Now suppose that /LOCK\DATA\BASE/ were entered in
the /LOCKED/ state. Then the value of /SOMEBODY\COUNT/
would be increased by 1.
.beginecl
.tabs 11,26,36
↑↑LOCK↑SOMEBODY\COUNT
↑UNLOCKED↑FALSE↑ 0
↑LOCKED↑TRUE↑ 0, 1
.endecl
By induction, it therefore follows that $any$
non-negative value is possible for /SOMEBODY\COUNT/
in the /LOCKED/ state.
.beginecl
.tabs 11,26,36
↑↑LOCK↑SOMEBODY\COUNT
↑UNLOCKED↑FALSE↑ 0
↑LOCKED↑TRUE↑ ≥ 0
.endecl
Now we turn to the possible effects of /UNLOCK\DATA\BASE/
on the value of /SOMEBODY\COUNT/. On entry the system must be
in the /LOCKED/ state, but the actions performed depend on
the value of /SOMEBODY\COUNT/. First suppose that
/SOMEBODY\COUNT/ is greater than zero. Then the value of
/SOMEBODY\COUNT/ is decremented by 1 and the system stays
in the /LOCKED/ state. Thus our information is unchanged.
.beginecl
.tabs 11,26,36
↑↑LOCK↑SOMEBODY\COUNT
↑UNLOCKED↑FALSE↑ 0
↑LOCKED↑TRUE↑ ≥ 0
.endecl
Now suppose that /SOMEBODY\COUNT/ is zero.
Then it remains zero, and the system goes into the /UNLOCKED/
state. This too adds no new information.
.beginecl
.tabs 11,26,36
↑↑LOCK↑SOMEBODY\COUNT
↑UNLOCKED↑FALSE↑ 0
↑LOCKED↑TRUE↑ ≥ 0
.endecl
We have now examined all possible execution paths, so we
now have all the information we can get about the value of
/SOMEBODY\COUNT/. We see now that we have the following
interesting relationships:
.beginecl
↑↑↑LOCK = FALSE ∀→ SOMEBODY\COUNT = 0
↑↑↑SOMEBODY\COUNT > 0 ∀→ LOCK = TRUE
.endecl
As described in section @optmap@, such a relationship
suggests a merging of the variables /LOCK/ and
/SOMEBODY\COUNT/. Let us introduce a new variable /COUNT1/
as follows:
.beginecl
.tabs 18,25,32,39,46,53,60
LOCK↑FALSE↑TRUE↑TRUE↑TRUE↑TRUE↑TRUE↑...
SOMEBODY\COUNT↑0↑0↑1↑2↑3↑4↑...
COUNT1↑0↑1↑2↑3↑4↑5↑...
.endecl
We therefore can replace constructs involving
/LOCK/ and /SOMEBODY\COUNT/ by constructs involving
only /COUNT1/:
.beginecl
.TABS 40
LOCK = FALSE↑COUNT1 = 0
LOCK ∀← NOT LOCK↑[) COUNT1 = 0 => COUNT1 ∀← 1;
↑ COUNT1 = 1 => COUNT1 ∀← 0;
↑ <impossible> (]
SOMEBODY\COUNT GT 0↑COUNT1 GT 1
SOMEBODY\COUNT ∀← SOMEBODY\COUNT + 1↑[) COUNT1 GT 0 =>
↑ COUNT1 ∀← COUNT1 + 1;
↑ <impossible> (]
SOMEBODY\COUNT ∀← SOMEBODY\COUNT - 1↑[) COUNT1 GT 0 =>
↑ COUNT1 ∀← COUNT1 - 1;
↑ <impossible> (]
.endecl
The cases labeled "<impossible>" are explicitly written as
such above because it takes a non-trivial bit of thinking
to prove that they are impossible. Of course, at substitution
time the impossible cases need not be inserted, or else they can
be left in for error checking purposes, because they should be
optimized out in the next few steps.
We thus can substitute these hunks of code into
the synchronization functions:
.beginecl
↑LOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
∞↑↑↑COUNT1 = 0 =>
∞↑↑↑↑[) [) COUNT1 = 0 => COUNT1 ∀← 1;
∞↑↑↑↑ COUNT1 = 1 => COUNT1 ∀← 0;
∞↑↑↑↑ <impossible> (];
↑↑↑↑↑ εVε(mutex) (];
∞↑↑↑[) COUNT1 GT 0 => COUNT1 ∀← COUNT1 + 1;
∞↑↑↑ <impossible> (];
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(SOMEBODY\SEM);
↑↑↑END;
↑UNLOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
∞↑↑↑COUNT1 GT 1 =>
↑↑↑↑↑BEGIN
∞↑↑↑↑↑[) COUNT1 GT 0 => COUNT1 ∀← COUNT1 - 1;
∞↑↑↑↑↑ <impossible> (];
↑↑↑↑↑↑εVε(SOMEBODY\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
∞↑↑↑[) COUNT1 = 0 => COUNT1 ∀← 1;
∞↑↑↑ COUNT1 = 1 => COUNT1 ∀← 0;
∞↑↑↑ <impossible> (]
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
There is plenty of opportunity here for elimination
of useless conditionals. First, for purposes of expositional
clarity let us put in some comments about known values of /COUNT1/
at relevant places in the code:
.beginecl
↑LOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑COUNT1 = 0 =>
∞↑↑↑↑[) IE "COUNT1 = 0";
↑↑↑↑↑ [) COUNT1 = 0 => COUNT1 ∀← 1;
↑↑↑↑↑ COUNT1 = 1 => COUNT1 ∀← 0;
↑↑↑↑↑ <impossible> (];
↑↑↑↑↑ εVε(mutex) (];
∞↑↑↑IE "COUNT1 ~ 0; BUT COUNT1 ≥ 0, ERGO COUNT1 GT 0";
↑↑↑↑[) COUNT1 GT 0 => COUNT1 ∀← COUNT1 + 1;
↑↑↑↑ <impossible> (];
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(SOMEBODY\SEM);
↑↑↑END;
↑UNLOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
∞↑↑↑IE "COUNT1 > 0 BY THE STATE ASSERTION";
↑↑↑↑εPε(mutex);
↑↑↑↑COUNT1 GT 1 =>
↑↑↑↑↑BEGIN
∞↑↑↑↑↑IE "COUNT1 > 1; BUT 1 > 0, ERGO COUNT1 GT 0";
↑↑↑↑↑↑[) COUNT1 GT 0 => COUNT1 ∀← COUNT1 - 1;
↑↑↑↑↑↑ <impossible> (];
↑↑↑↑↑↑εVε(SOMEBODY\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
∞↑↑↑IE "COUNT1 > 0 AND COUNT1 ≤ 1, ERGO COUNT1 = 1";
↑↑↑↑[) COUNT1 = 0 => COUNT1 ∀← 1;
↑↑↑↑ COUNT1 = 1 => COUNT1 ∀← 0;
↑↑↑↑ <impossible> (]
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
Next we can eliminate the useless conditionals
on the basis of this information:
.beginecl
↑LOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑COUNT1 = 0 =>
∞↑↑↑↑[) COUNT1 ∀← 1;
↑↑↑↑↑ εVε(mutex) (];
∞↑↑↑COUNT1 ∀← COUNT1 + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(SOMEBODY\SEM);
↑↑↑END;
↑UNLOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
%5|%*
↑↑↑↑εPε(mutex);
↑↑↑↑COUNT1 GT 1 =>
↑↑↑↑↑BEGIN
∞↑↑↑↑↑COUNT1 ∀← COUNT1 - 1;
↑↑↑↑↑↑εVε(SOMEBODY\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
∞↑↑↑COUNT1 ∀← 0;
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
Next we would like to simplify the code some more.
Motivated by the two assignments to /COUNT1/
appearing in each synchronization function,
we will find it convenient to take advantage of the following
equivalence transformations:
.beginecl
↑↑↑COUNT1 = 0 ∀→ ( COUNT1 ∀← 1 ∀↔ COUNT1 ∀← COUNT1 + 1 )
↑↑↑COUNT1 = 1 ∀→ ( COUNT1 ∀← 0 ∀↔ COUNT1 ∀← COUNT1 - 1 )
.endecl
Thus we find that we can alter two of the assignments in
preparation for code merging:
.beginecl
↑LOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑COUNT1 = 0 =>
∞↑↑↑↑[) COUNT1 ∀← COUNT1 + 1;
↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑COUNT1 ∀← COUNT1 + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(SOMEBODY\SEM);
↑↑↑END;
↑UNLOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑COUNT1 GT 1 =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑COUNT1 ∀← COUNT1 - 1;
↑↑↑↑↑↑εVε(SOMEBODY\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
∞↑↑↑COUNT1 ∀← COUNT1 - 1;
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
Now, by means of code merging and code motion,
we can simplify the multiple occurrences of
/COUNT1/↓_#∀←#_↓/COUNT1 + 1/ and /COUNT1/↓_#∀←#_↓/COUNT1 - 1/.
Note that the predicates in the conditions must be modified also.
.beginecl
↑LOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
∞↑↑↑COUNT1 ∀← COUNT1 + 1;
∞↑↑↑COUNT1 = 1 =>
%5|%*
↑↑↑↑↑ εVε(mutex);
%5|%*
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(SOMEBODY\SEM);
↑↑↑END;
↑UNLOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
∞↑↑↑COUNT1 ∀← COUNT1 - 1;
∞↑↑↑COUNT1 GT 0 =>
↑↑↑↑↑BEGIN
%5|%*
↑↑↑↑↑↑εVε(SOMEBODY\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
%5|%*
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
The next step is rather tricky. It involves
moving the operations on /SOMEBODY\SEM/ elsewhere
within their respective synchronization functions.
First let us look at the desired motion, and then
derive the justification for it.
.beginecl
↑LOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
∞↑↑↑εPε(SOMEBODY\SEM);
↑↑↑↑εPε(mutex);
↑↑↑↑COUNT1 ∀← COUNT1 + 1;
↑↑↑↑COUNT1 = 1 => εVε(mutex);
%5|%*
↑↑↑↑εVε(mutex);
↑↑↑END;
↑UNLOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
∞↑↑↑εVε(SOMEBODY\SEM);
↑↑↑↑COUNT1 ∀← COUNT1 - 1;
↑↑↑↑COUNT1 GT 0 =>
↑↑↑↑↑BEGIN
%5|%*
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
This semaphore motion is actually an odd combination
of a data mapping, an equivalence transformation,
and a code merging. In practice it may be easier to
handle this as a special case rather than going through
three separate steps.
The first step is to consider the possible values
of the counter $internal$ to the semaphore /SOMEBODY\SEM/.
These values are the negatives of the values of the
former variable /SOMEBODY\COUNT/, since all generated
semaphores except /mutex/ are at first assumed to be initially
zero. Let us therefore consider these values:
.beginecl
.tabs 18,25,32,39,46,53,60
COUNT1↑0↑1↑2↑3↑4↑5↑...
SOMEBODY\SEM↑0↑0↑-1↑-2↑-3↑-4↑...
.endecl
We note that /SOMEBODY\SEM = 1 - COUNT1/ except when /COUNT1 = 0/.
Furthermore we note that we perform a ↓_εPε_↓/(SOMEBODY\SEM)/ precisely
when /COUNT1 > 0/, and perform ↓_εVε_↓/(SOMEBODY\SEM)/ precisely
when /COUNT1 > 0/ also. Suppose now that we instead were to define
the values of /SOMEBODY\SEM/ as follows:
.beginecl
.tabs 18,25,32,39,46,53,60
COUNT1↑0↑1↑2↑3↑4↑5↑...
SOMEBODY\SEM↑1↑0↑-1↑-2↑-3↑-4↑...
.endecl
That is, in the "initial" state, /SOMEBODY\SEM = 1/.
Then /LOCK\DATA\BASE/ would have to perform ↓_εPε_↓/(SOMEBODY\SEM)/
even when /COUNT1 = 0/; but we know this is all right because
by definition /SOMEBODY\SEM = 1/ and so the εPε would not hang.
Similarly /UNLOCK\DATA\BASE/ would also have to perform
↓_εVε_↓/(SOMEBODY\SEM)/ even when /COUNT1 = 0/.
If we therefore introduce these operations and perform code
merging, we get the desired transformation, i.e. semaphore motion.
Note that when the code is merged for /LOCK\DATA\BASE/, the
↓_εPε_↓/(SOMEBODY\SEM)/ must be moved up $before$ the ↓_εPε_↓/(mutex)/.
This will generally be true when εPε operations are merged.
The next step merely involves merging the several
occurrences of ↓_εVε_↓/(mutex)/.
.beginecl
↑LOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(SOMEBODY\SEM);
↑↑↑↑εPε(mutex);
↑↑↑↑COUNT1 ∀← COUNT1 + 1;
%5|%*
↑↑↑↑εVε(mutex);
↑↑↑END;
↑UNLOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑εVε(SOMEBODY\SEM);
↑↑↑↑COUNT1 ∀← COUNT1 - 1;
%5|%*
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
It is now apparent that /COUNT1/ has become a useless
variable, and so it may be excised from the code.
.beginecl
↑LOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(SOMEBODY\SEM);
↑↑↑↑εPε(mutex);
%5|%*
↑↑↑↑εVε(mutex);
↑↑↑END;
↑UNLOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑εVε(SOMEBODY\SEM);
%5|%*
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
We have successfully eliminated $all$ the variables
from the code, and therefore may eliminate /mutex/ as well
(see section @optmutexelim@).
.beginecl
↑LOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(SOMEBODY\SEM);
%5|%*
%5|%*
↑↑↑END;
↑UNLOCK\DATA\BASE ∀←
↑↑EXPR()
↑↑↑BEGIN
%5|%*
↑↑↑↑εVε(SOMEBODY\SEM);
%5|%*
↑↑↑END;
.endecl
Thus, at long last, we have a solution which does
not seem to admit of further optimization:
.beginecl
↑LOCK\DATA\BASE ∀← EXPR()(εPε(SOMEBODY\SEM));
↑UNLOCK\DATA\BASE ∀← EXPR()(εVε(SOMEBODY\SEM));
.endecl
.section readers,The First Readers and Writers Problem
This problem is propounded in [{courtois}], among other places;
we have used it already as an example in section @salexample@.
There are a number of processes of two kinds, $readers$
and $writers$, and a data base.
Any number of readers may access the data base at a time, but if a writer
is accessing the data base no other process, whether reader or writer,
may also access it concurrently.
The SAL assertions for this problem are as follows:
.beginecl
<↑QUIESCENT IS WRITER\FLAG = FALSE
↑↑↑↑AND NUMBER\OF\READERS = 0,
↑READING IS WRITER\FLAG = FALSE
↑↑↑↑AND NUMBER\OF\READERS GT 0,
↑WRITING IS WRITER\FLAG = TRUE
↑↑↑↑AND NUMBER\OF\READERS = 0
↑READER DOES
↑↑BEGIN
↑↑↑ASSERT(QUIESCENT, READING, WRITING);
↑↑↑CIA("START\READ");
↑↑↑ASSERT(<QUIESCENT, READING> ==> <READING, READING>,
↑↑↑ ELSE WAIT);
↑↑↑IE "READ FROM DATA BASE";
↑↑↑ASSERT(READING);
↑↑↑CIA("END\READ");
↑↑↑ASSERT(READING AND NUMBER\OF\READERS GT 1 ==> READING,
↑↑↑ READING AND NUMBER\OF\READERS = 1 ==>
↑↑↑↑↑↑QUIESCENT THEN
↑↑↑↑↑↑TRY IF REVIVE(WRITER) POSSIBLE END\TRY);
↑↑END,
↑WRITER DOES
↑↑BEGIN
↑↑↑ASSERT(QUIESCENT, READING, WRITING);
↑↑↑CIA("BEGIN\WRITE");
↑↑↑ASSERT(QUIESCENT ==> WRITING,
↑↑↑ ELSE WAIT IN WRITER\QUEUE);
↑↑↑IE "WRITE INTO DATA BASE";
↑↑↑ASSERT(WRITING);
↑↑↑CIA("END\WRITE");
↑↑↑ASSERT(ALWAYS QUIESCENT THEN
↑↑↑ TRY EITHER IF REVIVE(ALL READER
↑↑↑ OUTOF READER\QUEUE)
↑↑↑ POSSIBLE
↑↑↑ OR IF REVIVE(WRITER
↑↑↑ OUTOF WRITER\QUEUE)
↑↑↑ POSSIBLE
↑↑↑ END\OR
↑↑↑ END\TRY);
↑↑END >
.endecl
The SAL synthesizer produces the following
code from these assertions:⊗⊗The SAL synthesizer actually
does not produce the /SELECT/ construct, since it does
not presently exist in the EL1 language, but rather
uses a function called /XEITHER/, which is similar
in spirit to /SELECT/ anyway, and so we will ignore
this quibble.⊗
.beginecl
↑START\READ ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑WRITER\FLAG = FALSE AND NUMBER\OF\READERS GT 0 OR
↑↑↑↑↑↑WRITER\FLAG = FALSE AND NUMBER\OF\READERS = 0 =>
↑↑↑↑↑NUMBER\OF\READERS ∀← NUMBER\OF\READERS + 1;
↑↑↑↑ENTERL(LASTRUN, READER);
↑↑↑↑LASTRUN ∀← NIL;
↑↑↑END;
.endecl
.beginecl
↑END\READ ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑WRITER\FLAG = FALSE AND NUMBER\OF\READERS GT 1 =>
↑↑↑↑↑NUMBER\OF\READERS ∀← NUMBER\OF\READERS + -1;
↑↑↑↑NUMBER\OF\READERS ∀← NUMBER\OF\READERS + -1;
↑↑↑↑WRITER α# NIL =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑LASTRUN α# NIL -> ENTERL(LASTRUN, INACTIVEQ);
↑↑↑↑↑↑LASTRUN ∀← REMOVEF(WRITER);
↑↑↑↑↑↑START\WRITE();
↑↑↑↑↑END;
↑↑↑END;
.endecl
.beginecl
↑START\WRITE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑WRITER\FLAG = FALSE AND NUMBER\OF\READERS = 0 =>
↑↑↑↑↑WRITER\FLAG ∀← NOT WRITER\FLAG;
↑↑↑↑ENTERL(LASTRUN, WRITER);
↑↑↑↑LASTRUN ∀← NIL;
↑↑↑END;
.endecl
.beginecl
↑END\WRITE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑WRITER\FLAG ∀← NOT WRITER\FLAG;
↑↑↑↑SELECT
↑↑↑↑↑[WRITER α# NIL] =>
↑↑↑↑↑↑BEGIN
↑↑↑↑↑↑↑LASTRUN α# NIL -> ENTERL(LASTRUN, INACTIVEQ);
↑↑↑↑↑↑↑LASTRUN ∀← REMOVEF(WRITER);
↑↑↑↑↑↑↑START\WRITE();
↑↑↑↑↑↑END;
↑↑↑↑↑[READER α# NIL] =>
↑↑↑↑↑↑REPEAT
↑↑↑↑↑↑↑LASTRUN α# NIL -> ENTERL(LASTRUN, INACTIVEQ);
↑↑↑↑↑↑↑LASTRUN ∀← REMOVEF(READER);
↑↑↑↑↑↑↑START\READ();
↑↑↑↑↑↑↑READER = NIL => NOTHING;
↑↑↑↑↑↑END;
↑↑↑↑END;
↑↑↑END;
.endecl
First we perform all translation except for the
/REVIVE/ actions. Also, for simplicity we will make the arbitrary
decision to treat /SELECT/ as if it were a simple LISP /COND/
statement, and so translate it immediately into code
using the /=>/ construct within blocks. (Recall that the
semantics of /SELECT/ specifically permit the compiler
to choose an arbitrary ordering of any kind.)
.beginecl
↑START\READ ∀←
↑↑EXPR()
↑↑↑BEGIN
∞↑↑↑εPε(mutex);
↑↑↑↑WRITER\FLAG = FALSE AND NUMBER\OF\READERS GT 0 OR
↑↑↑↑↑↑WRITER\FLAG = FALSE AND NUMBER\OF\READERS = 0 =>
∞↑↑↑↑[) NUMBER\OF\READERS ∀← NUMBER\OF\READERS + 1;
∞↑↑↑↑ εVε(MUTEX) (];
∞↑↑↑READER\COUNT ∀← READER\COUNT + 1;
∞↑↑↑εVε(mutex);
∞↑↑↑εPε(READER\SEM);
↑↑↑END;
.endecl
.beginecl
↑END\READ ∀←
↑↑EXPR()
↑↑↑BEGIN
∞↑↑↑εPε(mutex);
↑↑↑↑WRITER\FLAG = FALSE AND NUMBER\OF\READERS GT 1 =>
∞↑↑↑↑[) NUMBER\OF\READERS ∀← NUMBER\OF\READERS + -1;
∞↑↑↑↑ εVε(mutex) (];
↑↑↑↑NUMBER\OF\READERS ∀← NUMBER\OF\READERS + -1;
∞↑↑↑WRITER\COUNT GT 0 =>
↑↑↑↑↑BEGIN
∞↑↑↑↑↑REVIVE(WRITER);
∞↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
∞↑↑↑εVε(mutex);
↑↑↑END;
.endecl
.beginecl
↑START\WRITE ∀←
↑↑EXPR()
∞↑↑↑εPε(mutex);
↑↑↑BEGIN
↑↑↑↑WRITER\FLAG = FALSE AND NUMBER\OF\READERS = 0 =>
∞↑↑↑↑[) WRITER\FLAG ∀← NOT WRITER\FLAG;
∞↑↑↑↑ εVε(mutex) (];
∞↑↑↑WRITER\COUNT ∀← WRITER\COUNT + 1;
∞↑↑↑εVε(mutex);
∞↑↑↑εPε(WRITER\SEM);
↑↑↑END;
.endecl
.beginecl
↑END\WRITE ∀←
↑↑EXPR()
↑↑↑BEGIN
∞↑↑↑εPε(MUTEX);
↑↑↑↑WRITER\FLAG ∀← NOT WRITER\FLAG;
%5|%*
∞↑↑↑WRITER\COUNT GT 0 =>
↑↑↑↑↑BEGIN
∞↑↑↑↑↑REVIVE(WRITER);
∞↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
∞↑↑↑READER\COUNT GT 0 =>
↑↑↑↑↑REPEAT
∞↑↑↑↑↑REVIVE(READER)
∞↑↑↑↑↑READER\COUNT = 0 => εVε(mutex);
↑↑↑↑↑END;
%5|%*
∞↑↑↑εVε(mutex);
↑↑↑END;
.endecl
Next we extract the relevant code in order
to translate each occurrence of /REVIVE/:
.beginecl
↑START\READ ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑WRITER\FLAG = FALSE AND NUMBER\OF\READERS GT 0 OR
↑↑↑↑↑↑WRITER\FLAG = FALSE AND NUMBER\OF\READERS = 0 =>
↑↑↑↑↑[) NUMBER\OF\READERS ∀← NUMBER\OF\READERS + 1;
↑↑↑↑↑ εVε(MUTEX) (];
↑↑↑↑READER\COUNT ∀← READER\COUNT + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(READER\SEM);
↑↑↑END;
.endecl
.beginecl
↑END\READ ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑WRITER\FLAG = FALSE AND NUMBER\OF\READERS GT 1 =>
↑↑↑↑↑[) NUMBER\OF\READERS ∀← NUMBER\OF\READERS + -1;
↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑NUMBER\OF\READERS ∀← NUMBER\OF\READERS + -1;
↑↑↑↑WRITER\COUNT GT 0 =>
↑↑↑↑↑BEGIN
∞↑↑↑↑↑WRITER\COUNT ∀← WRITER\COUNT - 1;
∞↑↑↑↑↑WRITER\FLAG ∀← NOT WRITER\FLAG;
∞↑↑↑↑↑εVε(WRITER\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
.beginecl
↑START\WRITE ∀←
↑↑EXPR()
↑↑↑↑εPε(mutex);
↑↑↑BEGIN
↑↑↑↑WRITER\FLAG = FALSE AND NUMBER\OF\READERS = 0 =>
↑↑↑↑↑[) WRITER\FLAG ∀← NOT WRITER\FLAG;
↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑WRITER\COUNT ∀← WRITER\COUNT + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(WRITER\SEM);
↑↑↑END;
.endecl
.beginecl
↑END\WRITE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(MUTEX);
↑↑↑↑WRITER\FLAG ∀← NOT WRITER\FLAG;
↑↑↑↑WRITER\COUNT GT 0 =>
↑↑↑↑↑BEGIN
∞↑↑↑↑↑WRITER\COUNT ∀← WRITER\COUNT - 1;
∞↑↑↑↑↑WRITER\FLAG ∀← NOT WRITER\FLAG;
∞↑↑↑↑↑εVε(WRITER\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
↑↑↑↑READER\COUNT GT 0 =>
↑↑↑↑↑REPEAT
∞↑↑↑↑↑READER\COUNT ∀← READER\COUNT - 1;
∞↑↑↑↑↑NUMBER\OF\READERS ∀← NUMBER\OF\READERS + 1;
∞↑↑↑↑↑εVε(READER\SEM);
↑↑↑↑↑↑READER\COUNT = 0 => εVε(mutex);
↑↑↑↑↑END;
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
This is, of course, a working solution to the
problem. Some of the code can be optimized, however.
In /START\READ/, the condition which tests the state variables
can be simplified: first by combining the two logical terms
into one (and combining the /GT/ and %3=%* operations into
a /GE/ operation); next by deducing from the state information
that it is $always$ true that /NUMBER\OF\READERS#GE#0/,
and so the testing of that variable is useless and may be
eliminated:
.beginecl
↑START\READ ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
∞↑↑↑WRITER\FLAG = FALSE =>
↑↑↑↑↑[) NUMBER\OF\READERS ∀← NUMBER\OF\READERS + 1;
↑↑↑↑↑ εVε(MUTEX) (];
↑↑↑↑READER\COUNT ∀← READER\COUNT + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(READER\SEM);
↑↑↑END;
.endecl
In /END\READ/, several optimizations may
be made. The various occurrences of ↓_εVε_↓/(mutex)/
may be united via code merging (it is necessary to introduce
additional block structure to represent this correctly
in EL1). The two assignments
to /NUMBER\OF\READERS/ may also be merged, with an
appropriate modification to the predicate.
Next, it may be deduced from the state information
that /WRITE\FLAG#=#FALSE/, and so an equivalence
transformation may be made on the assignment to
/WRITE\FLAG/.⊗⊗Naturally, the SAL synthesizer also
realized this equivalence and so chose a function,
somewhat arbitrarily, to accomplish the state
change. The preference for /NOT/ over constant
functions apparently has to do with certain
internal heuristics for more complicated cases.⊗
Finally, it may be deduced from the state information that if
/NUMBER\OF\READERS#GT#1/, it is necessarily true also that
/WRITER\FLAG#=#FALSE/, and so the latter test need not be made:
.beginecl
↑END\READ ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
∞↑↑↑NUMBER\OF\READERS ∀← NUMBER\OF\READERS - 1;
∞↑↑↑BEGIN
∞↑↑↑↑NUMBER\OF\READERS GT 0 => NOTHING;
↑↑↑↑↑WRITER\COUNT GT 0 =>
↑↑↑↑↑↑BEGIN
↑↑↑↑↑↑↑WRITER\COUNT ∀← WRITER\COUNT - 1;
∞↑↑↑↑↑↑WRITER\FLAG ∀← TRUE;
↑↑↑↑↑↑↑εVε(WRITER\SEM);
↑↑↑↑↑↑END;
∞↑↑↑END;
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
In /START\WRITE/ there is little we can do except
perform another equivalence transformation, this time with
information derived from the predicate which conditionalizes
the assignment to /WRITER\FLAG/.
.beginecl
↑START\WRITE ∀←
↑↑EXPR()
↑↑↑↑εPε(mutex);
↑↑↑BEGIN
↑↑↑↑WRITER\FLAG = FALSE AND NUMBER\OF\READERS = 0 =>
∞↑↑↑↑[) WRITER\FLAG ∀← TRUE;
↑↑↑↑↑ εVε(mutex) (];
↑↑↑↑WRITER\COUNT ∀← WRITER\COUNT + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(WRITER\SEM);
↑↑↑END;
.endecl
In /END\WRITE/ we can again merge the various
occurrences of ↓_εVε_↓/(mutex)/ (once again, additional
block structure is needed to represent this in EL1).
We can also split the
first assignment to /WRITER\FLAG/, moving one copy into
the block conditionalized by /WRITER\COUNT#GT#0/ and one
copy after the conditional. Then we can use the fact that
/NOT#NOT#X#≡#X/ to cancel the two assignments in the
conditionalized block. Finally an equivalence transformation
shows that the remaining assignment to /WRITER\FLAG/
may be converted to an assignment of /FALSE/.
.beginecl
↑END\WRITE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(MUTEX);
%5|%*
∞↑↑↑BEGIN
↑↑↑↑↑WRITER\COUNT GT 0 =>
↑↑↑↑↑↑BEGIN
↑↑↑↑↑↑↑WRITER\COUNT ∀← WRITER\COUNT - 1;
%5|%*
↑↑↑↑↑↑↑εVε(WRITER\SEM);
%5|%*
↑↑↑↑↑↑END;
∞↑↑↑↑WRITE\FLAG ∀← FALSE;
↑↑↑↑↑READER\COUNT GT 0 =>
↑↑↑↑↑↑REPEAT
↑↑↑↑↑↑↑READER\COUNT ∀← READER\COUNT - 1;
↑↑↑↑↑↑↑NUMBER\OF\READERS ∀← NUMBER\OF\READERS + 1;
↑↑↑↑↑↑↑εVε(READER\SEM);
∞↑↑↑↑↑↑READER\COUNT = 0 => NOTHING;
↑↑↑↑↑↑END;
∞↑↑↑END;
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
The resulting code thus far is quite good.
One more trick could be used, namely a data mapping:
The variables /WRITER\FLAG/ and /NUMBER\OF\READERS/ could
be merged into a single variable /SWITCH/, essentially
by letting non-negative values correspond to values
of /NUMBER\OF\READERS/, and letting, say, /-1/ mean that
/WRITER\FLAG#=#TRUE/. It should be clear how to go about this,
however, and so it will not be detailed here.
As an interesting aside, however, let us consider
a PDP-10 timesharing system which provides a UUO /.PSEM/
which performs the εPε operation on a semaphore
pointed to by its effective address; furthermore let
/.VSEM/ be an alias for the /AOS/ instruction.
Then it is interesting to note what compact
(and what crystal-clear) PDP-10 code can be generated
by straightforwardly compiling the EL1 code above:
.beginecl
.tabs 9,25
VPOPJ:↑.VSEM MUTEX↑;useful common exit to come to
POPJ P,
STARTR:↑.PSEM MUTEX↑;code for START\READ
↑SKIPE WFLAG↑;skip if WRITER\FLAG is FALSE
↑ JRST SR1
↑AOS NREADR↑;increment NUMBER\OF\READERS
↑JRST VPOPJ
SR1:↑AOS RCOUNT↑;increment READER\COUNT
↑.VSEM MUTEX
↑.PSEM RSEM↑;εPε(READER\SEM)
↑POPJ P,
.endecl
.beginecl
.tabs 9,25
ENDR:↑.PSEM MUTEX↑;code for END\READ
↑SOSG NREADR↑;trivial skip optimization here
↑ SKIPG WCOUNT
↑ JRST ER1
↑SOS WCOUNT↑;decrement WRITER\COUNT
↑SETOM WFLAG↑;set WRITER\FLAG to TRUE
↑.VSEM WSEM↑;εPε(WRITER\SEM)
ER1:↑JRST VPOPJ
.endecl
.beginecl
.tabs 9,25
STARTW:↑.PSEM MUTEX↑;code for START\WRITE
↑SKIPN WFLAG↑;if WRITE\FLAG = FALSE
↑ SKIPE NREADR↑; and NUMBER\OF\READERS = 0
↑ JRST SW1
↑SETOM WFLAG↑; then set WRITER\FLAG to TRUE
↑JRST VPOPJ
SW1:↑AOS WCOUNT↑;otherwise increment WRITER\COUNT
↑.VSEM MUTEX
↑.PSEM WSEM↑; and perform εPε(WRITER\SEM)
↑POPJ P,
.endecl
.beginecl
.tabs 9,25
ENDW:↑.PSEM MUTEX↑;code for END\WRITE
↑SKIPG WCOUNT↑;if WRITER\COUNT GT 0
↑ JRST EW1
↑SOS WCOUNT↑; then decrement WRITER\COUNT
↑.VSEM WSEM↑; and release a writer
↑JRST EW3
EW1:↑SETZM WFLAG↑;otherwise set WRITE\FLAG to FALSE
↑SKIPG RCOUNT↑;now if NUMBER\OF\READERS GT 0
↑ JRST EW3
EW2:↑SOS RCOUNT↑; then loop trying to revive readers
↑AOS NREADR
↑.VSEM RSEM
↑SKIPE RCOUNT
↑ JRST EW2
EW3:↑JRST VPOPJ↑;finally exit
.endecl
Thus the entire solution, including the /VPOPJ/
routine, takes 44 (decimal) words of code, plus
4 words for variables and 2 for semaphores.
This example also suggests yet another
optimization technique. In this thesis we have assumed
that the "value" of the semaphore is $not$ accessible
(except via the εPε and εVε operations); this is the usual
convention. For most implementations of semaphores, however,
such as the one we have just used on a PDP-10, would permit
one to access such values. Since the counters
/READER\COUNT/ and /WRITER\COUNT/ were introduced specifically
to duplicate these values, such counters could in general be
eliminated at this low level, saving a few words (one
for each introduced counter).
.section cobbler,The Cobbler Problem
This problem will involve the problem
of reviving a process out of one waitset into another.
We will find it convenient to "cheat" a little bit
in order to get around the problem; rather than the
logical waitset approach mentioned in section
@bughelpswait@, we will use some special case state
analysis, which may also be a necessary technique in
an optimizer.
There is a cobbler who has a shop,
in which he normally sleeps all day.
There are a number of customers who want to have shoes
fixed. When a customer comes into the shop,
if someone is ahead of him he waits in the waiting room;
if no one is ahead of him, he wakes up the cobbler
and waits in a chair. When the cobbler finishes with
the shoes, he gives them to the customer in the chair,
who then leaves the shop, possibly after telling
the people in the waiting room that it is someone else's
turn. If there is more than one person in the waiting
room, there is a mad scramble to see who gets to the
cobbler next, i.e. there is no particular queueing discipline
in the waiting room.
The SAL assertions for this problem are as follows:
.beginecl
<↑QUIESCENT IS COBBLER\ACTIVE = FALSE
↑↑↑↑AND CUSTOMER\IN\SHOP = FALSE
↑↑↑↑AND SHOES\DONE = FALSE,
↑CUSTOMER\WAITING IS COBBLER\ACTIVE= TRUE
↑↑↑↑AND CUSTOMER\IN\SHOP = TRUE
↑↑↑↑AND SHOES\DONE = FALSE,
↑CUSTOMER\LEAVING IS COBBLER\ACTIVE = FALSE
↑↑↑↑AND CUSTOMER\IN\SHOP = TRUE
↑↑↑↑AND SHOES\DONE = TRUE,
↑CUSTOMER DOES
↑↑BEGIN
↑↑↑ASSERT(QUIESCENT, CUSTOMER\WAITING, CUSTOMER\LEAVING);
↑↑↑CIA("ARRIVE");
↑↑↑ASSERT(QUIESCENT ==> CUSTOMER\WAITING
↑↑↑↑↑↑AND STARTUP(COBBLER)
↑↑↑↑↑↑AND WAIT IN CHAIR,
↑↑↑ ELSE WAIT IN WAITING\ROOM);
↑↑↑ASSERT(CUSTOMER\LEAVING);
↑↑↑CIA("LEAVE");
↑↑↑ASSERT(CUSTOMER\LEAVING ==> QUIESCENT
↑↑↑↑↑↑AND TRY IF REVIVE(CUSTOMER
↑↑↑↑↑↑↑↑↑↑OUTOF WAITING\ROOM) POSSIBLE
↑↑↑↑↑↑ END\TRY);
↑↑END,
↑COBBLER DOES
↑↑BEGIN
↑↑↑ASSERT(CUSTOMER\WAITING);
↑↑↑CIA("FINISHES\SHOES");
↑↑↑ASSERT(CUSTOMER\WAITING ==> CUSTOMER\LEAVING
↑↑↑↑↑↑AND STARTUP(CUSTOMER OUTOF CHAIR)
↑↑↑↑↑↑AND WAIT);
↑↑END >
.endecl
Note that /STARTUP/ is used on two of the waitsets,
and /REVIVE/ on the third.
The code produced by the SAL synthesizer for
these assertions is as follows:
.beginecl
↑ARRIVE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑COBBLER\ACTIVE = FALSE
↑↑↑↑↑↑AND CUSTOMER\IN\SHOP = FALSE
↑↑↑↑↑↑AND SHOES\DONE = FALSE =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑ENTERL(LASTRUN, CHAIR);
↑↑↑↑↑↑LASTRUN ∀← NIL;
↑↑↑↑↑↑COBBLER\ACTIVE ∀← NOT COBBLER\ACTIVE;
↑↑↑↑↑↑CUSTOMER\IN\SHOP ∀← NOT CUSTOMER\IN\SHOP;
↑↑↑↑↑↑ENTERL(REMOVEF(COBBLER), INACTIVEQ);
↑↑↑↑↑END;
↑↑↑↑ENTERL(LASTRUN, WAITING\ROOM);
↑↑↑↑LASTRUN ∀← NIL;
↑↑↑END;
.endecl
.beginecl
↑LEAVE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑CUSTOMER\IN\SHOP ∀← NOT CUSTOMER\IN\SHOP;
↑↑↑↑SHOES\DONE ∀← NOT SHOES\DONE;
↑↑↑↑WAITING\ROOM α# NIL =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑LASTRUN α# NIL -> ENTERL(LASTRUN, INACTIVEQ);
↑↑↑↑↑↑LASTRUN ∀← REMOVEF(WAITING\ROOM);
↑↑↑↑↑↑ARRIVE();
↑↑↑↑↑END;
↑↑↑END;
.endecl
.beginecl
↑FINISHES\SHOES ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑ENTERL(LASTRUN, COBBLER);
↑↑↑↑LASTRUN ∀← NIL;
↑↑↑↑COBBLER\ACTIVE ∀← NOT COBBLER\ACTIVE;
↑↑↑↑SHOES\DONE ∀← NOT SHOES\DONE;
↑↑↑↑ENTERL(REMOVEF(CHAIR), INACTIVEQ);
↑↑↑END;
.endecl
Translating all of the code except the /REVIVE/
operation into semaphore code yields these functions:
.beginecl
↑ARRIVE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑COBBLER\ACTIVE = FALSE
↑↑↑↑↑↑AND CUSTOMER\IN\SHOP = FALSE
↑↑↑↑↑↑AND SHOES\DONE = FALSE =>
↑↑↑↑↑BEGIN
%5|%*
↑↑↑↑↑↑COBBLER\ACTIVE ∀← NOT COBBLER\ACTIVE;
↑↑↑↑↑↑CUSTOMER\IN\SHOP ∀← NOT CUSTOMER\IN\SHOP;
∞↑↑↑↑↑εVε(COBBLER\SEM);
∞↑↑↑↑↑εVε(mutex);
∞↑↑↑↑↑εPε(CHAIR\SEM);
↑↑↑↑↑END;
∞↑↑↑WAITING\ROOM\COUNT ∀← WAITING\ROOM\COUNT + 1;
∞↑↑↑εVε(mutex);
∞↑↑↑εPε(WAITING\ROOM\SEM);
↑↑↑END;
.endecl
.beginecl
↑LEAVE ∀←
↑↑EXPR()
↑↑↑BEGIN
∞↑↑↑εPε(mutex);
↑↑↑↑CUSTOMER\IN\SHOP ∀← NOT CUSTOMER\IN\SHOP;
↑↑↑↑SHOES\DONE ∀← NOT SHOES\DONE;
∞↑↑↑WAITING\ROOM\COUNT GT 0 =>
↑↑↑↑↑BEGIN
∞↑↑↑↑↑REVIVE(CUSTOMER OUTOF WAITING\ROOM);
∞↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
∞↑↑↑εVε(mutex);
↑↑↑END;
.endecl
.beginecl
↑FINISHES\SHOES ∀←
↑↑EXPR()
↑↑↑BEGIN
∞↑↑↑εPε(mutex);
↑↑↑↑COBBLER\ACTIVE ∀← NOT COBBLER\ACTIVE;
↑↑↑↑SHOES\DONE ∀← NOT SHOES\DONE;
∞↑↑↑εVε(CHAIR\SEM);
∞↑↑↑εVε(mutex);
∞↑↑↑εPε(COBBLER\SEM);
↑↑↑END;
.endecl
Next we would like to
extract the necessary code from the /ARRIVE/
function and put it in the /LEAVE/ function.
Unfortunately, the code to be extracted contains
a /WAIT/ action. It will be noted, however,
that whenever a /REVIVE(CUSTOMER#OUTOF#WAITING\ROOM)/
is performed the system is in the /QUIESCENT/ state,
and no other. Therefore whenever a /CUSTOMER/
is revived from the /WAITING\ROOM/ waitset it must
immediately enter the /CHAIR/ waitset. Therefore we
can safely place a ↓_εPε_↓/(CHAIR\SEM)/ after the
occurrence of ↓_εPε_↓/(WAITING\ROOM\SEM)/ and carry on:
.beginecl
↑ARRIVE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑COBBLER\ACTIVE = FALSE
↑↑↑↑↑↑AND CUSTOMER\IN\SHOP = FALSE
↑↑↑↑↑↑AND SHOES\DONE = FALSE =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑COBBLER\ACTIVE ∀← NOT COBBLER\ACTIVE;
↑↑↑↑↑↑CUSTOMER\IN\SHOP ∀← NOT CUSTOMER\IN\SHOP;
↑↑↑↑↑↑εVε(COBBLER\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑↑εPε(CHAIR\SEM);
↑↑↑↑↑END;
↑↑↑↑WAITING\ROOM\COUNT ∀← WAITING\ROOM\COUNT + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(WAITING\ROOM\SEM);
∞↑↑↑εPε(CHAIR\SEM);
↑↑↑END;
.endecl
.beginecl
↑LEAVE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑CUSTOMER\IN\SHOP ∀← NOT CUSTOMER\IN\SHOP;
↑↑↑↑SHOES\DONE ∀← NOT SHOES\DONE;
↑↑↑↑WAITING\ROOM\COUNT GT 0 =>
↑↑↑↑↑BEGIN
∞↑↑↑↑↑WAITING\ROOM\COUNT ∀← WAITING\ROOM\COUNT - 1;
∞↑↑↑↑↑COBBLER\ACTIVE ∀← NOT COBBLER\ACTIVE;
∞↑↑↑↑↑CUSTOMER\IN\SHOP ∀← NOT CUSTOMER\IN\SHOP;
∞↑↑↑↑↑εVε(COBBLER\SEM);
∞↑↑↑↑↑εVε(WAITING\ROOM\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
.beginecl
↑FINISHES\SHOES ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑COBBLER\ACTIVE ∀← NOT COBBLER\ACTIVE;
↑↑↑↑SHOES\DONE ∀← NOT SHOES\DONE;
↑↑↑↑εVε(CHAIR\SEM);
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(COBBLER\SEM);
↑↑↑END;
.endecl
At this point it may be noted that the state variables
are grossly redundant. In particular,
.beginecl
CUSTOMER\IN\SHOP = FALSE ∀→
↑↑↑↑↑COBBLER\ACTIVE = FALSE α∧ SHOES\DONE = FALSE
.endecl
and so two terms of the predicate in /ARRIVE/ may be eliminated:
.beginecl
↑ARRIVE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
%5|%*
∞↑↑↑CUSTOMER\IN\SHOP = FALSE =>
%5|%*
↑↑↑↑↑BEGIN
↑↑↑↑↑↑COBBLER\ACTIVE ∀← NOT COBBLER\ACTIVE;
↑↑↑↑↑↑CUSTOMER\IN\SHOP ∀← NOT CUSTOMER\IN\SHOP;
↑↑↑↑↑↑εVε(COBBLER\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑↑εPε(CHAIR\SEM);
↑↑↑↑↑END;
↑↑↑↑WAITING\ROOM\COUNT ∀← WAITING\ROOM\COUNT + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(WAITING\ROOM\SEM);
↑↑↑↑εPε(CHAIR\SEM);
↑↑↑END;
.endecl
It is now seen that the variables /COBBLER\ACTIVE/
and /SHOES\DONE/ are totally useless and may be excised from
the code:
.beginecl
↑ARRIVE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑CUSTOMER\IN\SHOP = FALSE =>
↑↑↑↑↑BEGIN
%5|%*
↑↑↑↑↑↑CUSTOMER\IN\SHOP ∀← NOT CUSTOMER\IN\SHOP;
↑↑↑↑↑↑εVε(COBBLER\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑↑εPε(CHAIR\SEM);
↑↑↑↑↑END;
↑↑↑↑WAITING\ROOM\COUNT ∀← WAITING\ROOM\COUNT + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(WAITING\ROOM\SEM);
↑↑↑↑εPε(CHAIR\SEM);
↑↑↑END;
.endecl
.beginecl
↑LEAVE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑CUSTOMER\IN\SHOP ∀← NOT CUSTOMER\IN\SHOP;
%5|%*
↑↑↑↑WAITING\ROOM\COUNT GT 0 =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑WAITING\ROOM\COUNT ∀← WAITING\ROOM\COUNT - 1;
%5|%*
↑↑↑↑↑↑CUSTOMER\IN\SHOP ∀← NOT CUSTOMER\IN\SHOP;
↑↑↑↑↑↑εVε(COBBLER\SEM);
↑↑↑↑↑↑εVε(WAITING\ROOM\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
.beginecl
↑FINISHES\SHOES ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
%5|%*
%5|%*
↑↑↑↑εVε(CHAIR\SEM);
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(COBBLER\SEM);
↑↑↑END;
.endecl
Next we may split the first assignment to
/CUSTOMER\IN\SHOP/ in the /LEAVE/ function,
and then perform code cancellation:
.beginecl
↑LEAVE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
%5|%*
↑↑↑↑WAITING\ROOM\COUNT GT 0 =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑WAITING\ROOM\COUNT ∀← WAITING\ROOM\COUNT - 1;
%5|%*
↑↑↑↑↑↑εVε(COBBLER\SEM);
↑↑↑↑↑↑εVε(WAITING\ROOM\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
↑↑↑↑CUSTOMER\IN\SHOP ∀← NOT CUSTOMER\IN\SHOP;
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
Next we may construct the following data mapping
on the basis of state information (the entire derivation
will not be given here, as it is analogous to the data
mapping used in section @exclusion@):
.beginecl
.tabs 25,32,39,46,53,60
CUSTOMER\IN\SHOP↑FALSE↑TRUE↑TRUE↑TRUE↑TRUE↑...
WAITING\ROOM\COUNT↑0↑0↑1↑2↑3↑...
COUNT1↑0↑1↑2↑3↑4↑...
.endecl
Then we may rewrite the functions in terms of /COUNT1/
as follows:
.beginecl
↑ARRIVE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
∞↑↑↑COUNT1 = 0 =>
↑↑↑↑↑BEGIN
∞↑↑↑↑↑COUNT1 ∀← COUNT1 + 1;
↑↑↑↑↑↑εVε(COBBLER\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑↑εPε(CHAIR\SEM);
↑↑↑↑↑END;
∞↑↑↑COUNT1 ∀← COUNT1 + 1;
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(WAITING\ROOM\SEM);
↑↑↑↑εPε(CHAIR\SEM);
↑↑↑END;
.endecl
.beginecl
↑LEAVE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
∞↑↑↑COUNT1 GT 1 =>
↑↑↑↑↑BEGIN
∞↑↑↑↑↑COUNT1 ∀← COUNT1 - 1;
↑↑↑↑↑↑εVε(COBBLER\SEM);
↑↑↑↑↑↑εVε(WAITING\ROOM\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑END;
∞↑↑↑COUNT1 ∀← COUNT1 - 1;
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
.beginecl
↑FINISHES\SHOES ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑εVε(CHAIR\SEM);
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(COBBLER\SEM);
↑↑↑END;
.endecl
(The reader should convince himself by consulting chapter
@chapoptimize@ and comparing with section @exclusion@
that the transformations are indeed correct.)
Next we may perform two code mergings, one in
/ARRIVE/ and two in /LEAVE/:
.beginecl
↑ARRIVE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
∞↑↑↑COUNT1 ∀← COUNT1 + 1;
∞↑↑↑COUNT1 = 1 =>
↑↑↑↑↑BEGIN
%5|%*
↑↑↑↑↑↑εVε(COBBLER\SEM);
↑↑↑↑↑↑εVε(mutex);
↑↑↑↑↑↑εPε(CHAIR\SEM);
↑↑↑↑↑END;
%5|%*
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(WAITING\ROOM\SEM);
↑↑↑↑εPε(CHAIR\SEM);
↑↑↑END;
.endecl
.beginecl
↑LEAVE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
∞↑↑↑COUNT1 ∀← COUNT1 - 1;
∞↑↑↑COUNT1 GT 0 ->
↑↑↑↑↑BEGIN
%5|%*
↑↑↑↑↑↑εVε(COBBLER\SEM);
↑↑↑↑↑↑εVε(WAITING\ROOM\SEM);
%5|%*
↑↑↑↑↑END;
%5|%*
↑↑↑↑εVε(mutex);
↑↑↑END;
.endecl
.beginecl
↑FINISHES\SHOES ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εPε(mutex);
↑↑↑↑εVε(CHAIR\SEM);
↑↑↑↑εVε(mutex);
↑↑↑↑εPε(COBBLER\SEM);
↑↑↑END;
.endecl
(Note that the block structure of /LEAVE/ has been
simplified above after the code merging.)
At this point we have a situation almost
identical to that in section @exclusion@:
we would like to perform some semaphore motion
on /WAITING\ROOM\SEM/
and thereby eliminate /COUNT1/, but cannot quite
because of the occurrences of ↓_εVε_↓/(COBBLER\SEM)/.
At this point, then, we will pull a very tricky "theorem",
a corollary to that of section @optmutexelim@,
out of a hat: $if$ /mutex/ $is eliminated because all
variables have been eliminated, then there is no mutual exclusion
to pass; therefore the extracted code may be put back in
the revived process$.
Another corollary is: $if ↓_assuming_↓ that$ /mutex/ $may be
eliminated will indeed permit its eventual elimination,
then it may indeed be (tentatively) eliminated$.
These "theorems" are not particularly obvious, but
a great deal of thought has convinced the author,
intuitively at least, that they are correct.
Proceeding on this assumption then, we shall eliminate
/mutex/ tentatively, then move the occurrence of
↓_εVε_↓/(COBBLER\SEM)/ which was extracted for a /REVIVE/
back from /LEAVE/ to /ARRIVE/:
.beginecl
↑ARRIVE ∀←
↑↑EXPR()
↑↑↑BEGIN
%5|%*
↑↑↑↑COUNT1 ∀← COUNT1 + 1;
↑↑↑↑COUNT1 = 1 =>
↑↑↑↑↑BEGIN
↑↑↑↑↑↑εVε(COBBLER\SEM);
%5|%*
↑↑↑↑↑↑εPε(CHAIR\SEM);
↑↑↑↑↑END;
∞↑↑↑εVε(COBBLER\SEM);
%5|%*
↑↑↑↑εPε(WAITING\ROOM\SEM);
↑↑↑↑εPε(CHAIR\SEM);
↑↑↑END;
.endecl
.beginecl
↑LEAVE ∀←
↑↑EXPR()
↑↑↑BEGIN
%5|%*
↑↑↑↑COUNT1 ∀← COUNT1 - 1;
↑↑↑↑COUNT1 GT 0 ->
↑↑↑↑↑BEGIN
%5|%*
↑↑↑↑↑↑εVε(WAITING\ROOM\SEM);
↑↑↑↑↑END;
%5|%*
↑↑↑END;
.endecl
.beginecl
↑FINISHES\SHOES ∀←
↑↑EXPR()
↑↑↑BEGIN
%5|%*
↑↑↑↑εVε(CHAIR\SEM);
%5|%*
↑↑↑↑εPε(COBBLER\SEM);
↑↑↑END;
.endecl
Now, at last, using the same semaphore motion
technique used in section @exclusion@ (which, recall,
requires altering the initial value of
/WAITING\ROOM\SEM/), we may merge some code, eliminate the variable
/COUNT1/, and achieve this result:
.beginecl
↑ARRIVE ∀←
↑↑EXPR()
↑↑↑BEGIN
%5|%*
%5|%*
↑↑↑↑εVε(COBBLER\SEM);
↑↑↑↑εPε(WAITING\ROOM\SEM);
↑↑↑↑εPε(CHAIR\SEM);
↑↑↑END;
.endecl
.beginecl
↑LEAVE ∀←
↑↑EXPR()
↑↑↑BEGIN
%5|%*
↑↑↑↑↑↑εVε(WAITING\ROOM\SEM);
%5|%*
↑↑↑END;
.endecl
.beginecl
↑FINISHES\SHOES ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εVε(CHAIR\SEM);
↑↑↑↑εPε(COBBLER\SEM);
↑↑↑END;
.endecl
We see then that our original assumtion that
/mutex/ may be eliminated has been vindicated,
and so by our (presumed) theorem the entire thing
has succeeded. The final synchronization
functions are therefore:
.beginecl
↑ARRIVE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εVε(COBBLER\SEM);
↑↑↑↑εPε(WAITING\ROOM\SEM);
↑↑↑↑εPε(CHAIR\SEM);
↑↑↑END;
.endecl
.beginecl
↑LEAVE ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑↑↑εVε(WAITING\ROOM\SEM);
↑↑↑END;
.endecl
.beginecl
↑FINISHES\SHOES ∀←
↑↑EXPR()
↑↑↑BEGIN
↑↑↑↑εVε(CHAIR\SEM);
↑↑↑↑εPε(COBBLER\SEM);
↑↑↑END;
.endecl
.chapter chapconclude,Conclusions and Future Work
It would seem reasonable to conclude from
our considerations that code extraction is a viable
technique for translating the /REVIVE/ construct.
It is furthermore primarily the application
of optimization techniques which makes the code
extraction method feasible and even profitable,
since the resulting code is in certain cases
much simpler than the equivalent CI code.
One problem with the code extraction technique
is that it does not handle extracted /WAIT/ actions
well; we have had to resort to special case analyses
in order to get around this in our examples.
Perhaps in such cases the /urgentcount/ approach
could be used as an alternative.
In fact, a rich area of further study would be the
consideration of using a hybrid technique involving
both /urgentcount/ and code extraction,
or both state splitting and code extraction for that
matter.
It may also be profitable to investigate the kinds
of situations in which neither code extraction
nor /urgentcount/ is needed, i.e. cases in which
brute force translation suffices.
The problem of circularly nested /REVIVE/
operations also deserves further attention.
It seems also that code optimization may generally be
a good thing to apply routinely to automatically
generated code; for example, the SAL synthesizer
itself might profit from a rear-end optimizer to
condense the conditionals in the CI code.⊗⊗In fact some
amount of optimization has been built in already.⊗
On the other hand, many of the translation techniques presented here
may find applicability in translating other kinds of
synchronization primitives such as monitors into
semaphores; in particular, they might be extended to
apply to more general CI code, and not just the restricted
types of code output by the SAL synthesizer.
In any case, it has been clearly demonstrated
in this thesis that one could
build an entire system composed of the SAL synthesizer
and verifier, the semaphore code generator and optimizer,
and the EL1 compiler, which as a pipeline processor
would accept very-high-level synchronization assertions
and mechanically produce running, working, efficient machine
language synchronization code.
This is a great advance from the previous state of the art,
which consisted primarily of various clever programmers
coding up semaphore solutions, usually incorrect at that,
by hand for individual problems. The new system
which this work and the work of Griffiths would comprise
is the first large-scale, practical high-level language
system for generating synchronization code.
Practical experience indicates that it is much easier
to specify concurrent processes in terms of SAL
than in terms of any other formalism yet proposed;
the work of this thesis shows that one can nevertheless
have the efficiency of a semaphore implementation
by having the system automatically generate semaphore code.
.next page
.begin "acknowledgements"
.odd heading(↓_%5Acknowledgements,,Page {page!}_↓)
.even heading(↓_%5Page {page!},,Acknowledgements_↓)
.every footing(↓_%5Acknowledgements,,Acknowledgements_↓)
.group skip 7
.once nofill indent 0 center
.select chapterheadfont
Acknowledgements
.skip 4
.send contents ⊂
.begin "acknowledgements contents"
.skip 1
%5Acknowledgements→{page!}
.end "acknowledgements contents" ⊃
.nofill center
.begin group
I would like to thank
.skip
Patricia Griffiths
.skip
for the many hours spent with me this past year,
explaining to me the intricacies of SAL,
helping me develop the notion of semaphore optimization,
and listening to my crazy ideas and digressions.
.end
.skip 3
.begin group
I would like to thank
.skip
Charles J. Prenner
.skip
my thesis advisor,
who first set me to thinking about synchronization in AM 219,
for the many hours spent advising me on my thesis,
helping me understand the subtleties of synchronization problems,
and listening to my ideas on semaphores,
whether thesis-related or not.
.end
.skip 3
.begin group
I would like to thank
.skip
Irene Greif
and
Carl E. Hewitt
.skip
of the M.I.T. AI Lab
for pointing me at helpful papers,
and for letting me bounce my ideas off them.
.end
.skip 3
.begin group
I would like to thank
.skip
the many people at Harvard and M.I.T.
.skip
who listened to me prattle on about my thesis
more for my benefit than theirs.
.end
.skip 3
.begin group
Finally, I would like to thank
.skip
my parents and brother
.skip
for putting up with me while I wrote this thesis,
out of the house at 7:00 AM,
never home for dinner,
typing away from early morning until after midnight.
.end
.group skip 10
. << ridiculous snoopy character >>
%7A%*
.end "acknowledgements"
.portion bibliography
.begin "bibliography block"
.odd heading(↓_%5References,,Page {page!}_↓)
.even heading(↓_%5Page {page!},,References_↓)
.every footing(↓_%5References,,References_↓)
.group skip 7
.once nofill indent 0 center
.select chapterheadfont
References
.skip 4
.send contents ⊂
.begin "references contents"
.skip 1
%5References→{page!}
.end "references contents" ⊃
.fill
.single space
.select textfont
.indent 0,10
.receive
.end "bibliography block"
.portion contents
.nofill
.tabs 8,14,22,32
.count page printing "i"
.odd heading(↓_%5Table of Contents,,Page {page!}_↓)
.even heading(↓_%5Page {page!},,Table of Contents_↓)
.every footing(↓_%5Table of Contents,,Table of Contents_↓)
.begin "contents!block"
.begin "temp99"
.next page
.center
.select chapterheadfont
Table of Contents
.end "temp99"
.skip 3
.indent 0,0
.select sectionheadfont
.receive
.end "contents!block"
ββ